Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2098
Grpcgrp 18861 Rngcrng 20055 |
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-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-abl 19701 df-rng 20056 |
This theorem is referenced by: rngacl
20065 rng0cl
20066 rngrz
20069 rngmneg1
20070 rngmneg2
20071 rngm2neg
20072 rngsubdi
20074 rngsubdir
20075 prdsrngd
20079 subrngsubg
20450 cntzsubrng
20465 rnglidlmcl
21073 rnglidl0
21086 rnglidl1
21089 2idlcpblrng
21126 rngqiprngimfolem
21141 rngqiprngimf1lem
21145 rngqiprngghm
21150 rngqiprngimf1
21151 rngqiprngimfo
21152 rngqiprngfulem3
21164 rngqiprngfulem4
21165 rngqiprngfulem5
21166 pzriprnglem4
21367 pzriprnglem10
21373 |