Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
class class class wbr 5149 ≈ cen 8936
≼ 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-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-f1o 6551 df-en 8940 df-dom 8941 |
This theorem is referenced by: domdifsn
9054 xpdom1g
9069 domunsncan
9072 sdomdomtr
9110 domen2
9120 mapdom2
9148 phpOLD
9222 unxpdom2
9254 sucxpdom
9255 xpfir
9266 fodomfi
9325 cardsdomelir
9968 infxpenlem
10008 xpct
10011 infpwfien
10057 inffien
10058 mappwen
10107 iunfictbso
10109 djuxpdom
10180 cdainflem
10182 djuinf
10183 djulepw
10187 ficardun2
10197 ficardun2OLD
10198 unctb
10200 infdjuabs
10201 infunabs
10202 infdju
10203 infdif
10204 infxpdom
10206 pwdjudom
10211 infmap2
10213 fictb
10240 cfslb
10261 fin1a2lem11
10405 fnct
10532 unirnfdomd
10562 iunctb
10569 alephreg
10577 cfpwsdom
10579 gchdomtri
10624 canthp1lem1
10647 pwfseqlem5
10658 pwxpndom
10661 gchdjuidm
10663 gchxpidm
10664 gchpwdom
10665 gchhar
10674 inttsk
10769 inar1
10770 tskcard
10776 znnen
16155 qnnen
16156 rpnnen
16170 rexpen
16171 aleph1irr
16189 cygctb
19760 1stcfb
22949 2ndcredom
22954 2ndcctbss
22959 hauspwdom
23005 tx2ndc
23155 met1stc
24030 met2ndci
24031 re2ndc
24317 opnreen
24347 ovolctb2
25009 ovolfi
25011 uniiccdif
25095 dyadmbl
25117 opnmblALT
25120 vitali
25130 mbfimaopnlem
25172 mbfsup
25181 aannenlem3
25843 dmvlsiga
33127 sigapildsys
33160 omssubadd
33299 carsgclctunlem3
33319 finminlem
35203 phpreu
36472 lindsdom
36482 mblfinlem1
36525 pellexlem4
41570 pellexlem5
41571 pr2dom
42278 tr3dom
42279 nnfoctb
43734 ioonct
44250 subsaliuncl
45074 caragenunicl
45240 aacllem
47848 |