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 7353 |
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 2707 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 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 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 7356 |
This theorem is referenced by: mapssfset
8785 mapdom2
9088 relexpsucrd
14910 relexpsucld
14911 relexpreld
14917 relexpdmd
14921 relexprnd
14925 relexpfldd
14927 relexpaddd
14931 dfrtrclrec2
14935 relexpindlem
14940 oveqprc
17056 setsnidOLD
17074 ressbasOLD
17111 resslemOLD
17115 ressinbas
17118 ressress
17121 oduval
18169 oduleval
18170 gsum0
18531 efmndbas
18673 oppgval
19116 oppgplusfval
19117 mgpval
19890 opprval
20035 srasca
20631 srascaOLD
20632 rlmsca2
20655 dsmmval
21125 dsmmfi
21129 resspsrbas
21368 mpfrcl
21479 psrbaspropd
21590 mplbaspropd
21592 evl1fval1
21681 qtopres
23033 fgabs
23214 tnglemOLD
23981 tngds
23995 tngdsOLD
23996 tcphval
24566 resvsca
32004 resvlemOLD
32006 mapco2g
40975 mzpmfp
41008 mendbas
41449 naryfvalixp
46647 1aryenef
46663 2aryenef
46674 |