Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → wi 4
∧ wa 396 = wceq 1541
∈ wcel 2106 Vcvv 3443
∅c0 4280 dom cdm 5631
Rel wrel 5636 (class class class)co 7351 |
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 |
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-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-xp 5637 df-rel 5638 df-dm 5641 df-iota 6445 df-fv 6501 df-ov 7354 |
This theorem is referenced by: mapssfset
8747 mapdom2
9050 relexpsucrd
14878 relexpsucld
14879 relexpreld
14885 relexpdmd
14889 relexprnd
14893 relexpfldd
14895 relexpaddd
14899 dfrtrclrec2
14903 relexpindlem
14908 oveqprc
17024 setsnidOLD
17042 ressbasOLD
17079 resslemOLD
17083 ressinbas
17086 ressress
17089 oduval
18137 oduleval
18138 gsum0
18499 efmndbas
18641 oppgval
19084 oppgplusfval
19085 mgpval
19858 opprval
20003 srasca
20599 srascaOLD
20600 rlmsca2
20623 dsmmval
21093 dsmmfi
21097 resspsrbas
21336 mpfrcl
21447 psrbaspropd
21558 mplbaspropd
21560 evl1fval1
21649 qtopres
23001 fgabs
23182 tnglemOLD
23949 tngds
23963 tngdsOLD
23964 tcphval
24534 resvsca
31947 resvlemOLD
31949 mapco2g
40946 mzpmfp
40979 mendbas
41420 naryfvalixp
46616 1aryenef
46632 2aryenef
46643 |