Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1533
∈ wcel 2098 ‘cfv 6536 (class class class)co 7404
Basecbs 17151 +gcplusg 17204 Grpcgrp 18861 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905
ax-6 1963 ax-7 2003 ax-8 2100
ax-9 2108 ax-ext 2697 ax-nul 5299 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2704 df-cleq 2718 df-clel 2804 df-ne 2935 df-ral 3056 df-rex 3065 df-rab 3427 df-v 3470 df-sbc 3773 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-br 5142 df-iota 6488 df-fv 6544 df-ov 7407 df-mgm 18571 df-sgrp 18650 df-mnd 18666 df-grp 18864 |
This theorem is referenced by: dfgrp3
18965 xpsinv
18986 xpsgrpsub
18987 nmzsubg
19090 eqger
19103 lringuplu
20442 rnglidl1
21089 rngqiprngimfo
21152 rngqiprngfulem3
21164 cphpyth
25095 ghmquskerlem3
33037 evls1addd
33157 ply1degltlss
33172 q1pdir
33178 r1pcyc
33182 r1padd1
33183 r1plmhm
33185 evls1maprhm
33278 algextdeglem8
33301 aks6d1c1p3
41485 grpcominv1
41624 rhmmpl
41663 mplmapghm
41666 evlsmaprhm
41680 evladdval
41685 selvadd
41698 |