Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ghom Structured version   Unicode version

Definition df-ghom 21938
 Description: Define the set of group homomorphisms from to . (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-ghom GrpOpHom
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-ghom
StepHypRef Expression
1 cghom 21937 . 2 GrpOpHom
2 vg . . 3
3 vh . . 3
4 cgr 21766 . . 3
52cv 1651 . . . . . . 7
65crn 4871 . . . . . 6
73cv 1651 . . . . . . 7
87crn 4871 . . . . . 6
9 vf . . . . . . 7
109cv 1651 . . . . . 6
116, 8, 10wf 5442 . . . . 5
12 vx . . . . . . . . . . 11
1312cv 1651 . . . . . . . . . 10
1413, 10cfv 5446 . . . . . . . . 9
15 vy . . . . . . . . . . 11
1615cv 1651 . . . . . . . . . 10
1716, 10cfv 5446 . . . . . . . . 9
1814, 17, 7co 6073 . . . . . . . 8
1913, 16, 5co 6073 . . . . . . . . 9
2019, 10cfv 5446 . . . . . . . 8
2118, 20wceq 1652 . . . . . . 7
2221, 15, 6wral 2697 . . . . . 6
2322, 12, 6wral 2697 . . . . 5
2411, 23wa 359 . . . 4
2524, 9cab 2421 . . 3
262, 3, 4, 4, 25cmpt2 6075 . 2
271, 26wceq 1652 1 GrpOpHom
 Colors of variables: wff set class This definition is referenced by:  elghomlem1  21941
 Copyright terms: Public domain W3C validator