Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 = wceq 1541
∈ wcel 2106 ‘cfv 6491 1st
c1st 7909 GrpOpcgr 29229
AbelOpcablo 29284 RingOpscrngo 36248 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-sep 5254 ax-nul 5261 ax-pr 5382 ax-un 7662 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5528 df-xp 5636 df-rel 5637 df-cnv 5638 df-co 5639 df-dm 5640 df-rn 5641 df-iota 6443 df-fun 6493 df-fn 6494 df-f 6495 df-fv 6499 df-ov 7352 df-1st 7911 df-2nd 7912 df-ablo 29285 df-rngo 36249 |
This theorem is referenced by: rngone0
36265 rngogcl
36266 rngoaass
36268 rngorcan
36271 rngolcan
36272 rngo0cl
36273 rngo0rid
36274 rngo0lid
36275 rngolz
36276 rngorz
36277 rngosn3
36278 rngonegcl
36281 rngoaddneg1
36282 rngoaddneg2
36283 rngosub
36284 rngodm1dm2
36286 rngorn1
36287 rngonegmn1l
36295 rngonegmn1r
36296 rngogrphom
36325 rngohom0
36326 rngohomsub
36327 rngokerinj
36329 keridl
36386 dmncan1
36430 |