Colors of
variables: wff
setvar class |
Syntax hints: ∃wex 1782 Rel wrel 5682
–1-1→wf1 6541 ≼
cdom 8937 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 df-ss 3966 df-opab 5212 df-xp 5683 df-rel 5684 df-dom 8941 |
This theorem is referenced by: relsdom
8946 brdomg
8952 brdomgOLD
8953 brdomi
8954 brdomiOLD
8955 ctex
8959 domssl
8994 domssr
8995 domtr
9003 undom
9059 undomOLD
9060 xpdom2
9067 xpdom1g
9069 domunsncan
9072 sbth
9093 sbthcl
9095 dom0OLD
9103 fodomr
9128 pwdom
9129 domssex
9138 mapdom1
9142 mapdom2
9148 domtrfil
9195 sbthfi
9202 0sdom1dom
9238 1sdom2dom
9247 fineqv
9263 infsdomnn
9305 infsdomnnOLD
9306 infn0ALT
9308 elharval
9556 harword
9558 domwdom
9569 unxpwdom
9584 infdifsn
9652 infdiffi
9653 ac10ct
10029 djudom2
10178 djuinf
10183 infdju1
10184 pwdjuidm
10186 djulepw
10187 infdjuabs
10201 infunabs
10202 pwdjudom
10211 infpss
10212 infmap2
10213 fictb
10240 infpssALT
10308 fin34
10385 ttukeylem1
10504 fodomb
10521 wdomac
10522 brdom3
10523 iundom2g
10535 iundom
10537 infxpidm
10557 gchdomtri
10624 pwfseq
10659 pwxpndom2
10660 pwxpndom
10661 pwdjundom
10662 gchdjuidm
10663 gchpwdom
10665 gchaclem
10673 reexALT
12968 hashdomi
14340 1stcrestlem
22956 hauspwdom
23005 ufilen
23434 ovoliunnul
25024 ovoliunnfl
36530 voliunnfl
36532 volsupnfl
36533 nnfoctb
43734 rn1st
43978 meadjiun
45182 caragenunicl
45240 |