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

Definition df-ghom 23998
 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 23997 . 2 GrpOpHom
2 vg . . 3
3 vh . . 3
4 cgr 23826 . . 3
52cv 1369 . . . . . . 7
65crn 4950 . . . . . 6
73cv 1369 . . . . . . 7
87crn 4950 . . . . . 6
9 vf . . . . . . 7
109cv 1369 . . . . . 6
116, 8, 10wf 5523 . . . . 5
12 vx . . . . . . . . . . 11
1312cv 1369 . . . . . . . . . 10
1413, 10cfv 5527 . . . . . . . . 9
15 vy . . . . . . . . . . 11
1615cv 1369 . . . . . . . . . 10
1716, 10cfv 5527 . . . . . . . . 9
1814, 17, 7co 6201 . . . . . . . 8
1913, 16, 5co 6201 . . . . . . . . 9
2019, 10cfv 5527 . . . . . . . 8
2118, 20wceq 1370 . . . . . . 7
2221, 15, 6wral 2799 . . . . . 6
2322, 12, 6wral 2799 . . . . 5
2411, 23wa 369 . . . 4
2524, 9cab 2439 . . 3
262, 3, 4, 4, 25cmpt2 6203 . 2
271, 26wceq 1370 1 GrpOpHom
 Colors of variables: wff setvar class This definition is referenced by:  elghomlem1  24001
 Copyright terms: Public domain W3C validator