Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → wi 4
class class class wbr 5109 ≈ cen 8886
≼ cdom 8887 ≺
csdm 8888 |
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 3449 df-dif 3917 df-br 5110 df-sdom 8892 |
This theorem is referenced by: domdifsn
9004 sucdom2OLD
9032 sdomnsym
9048 sdomdomtr
9060 domsdomtr
9062 sdomtr
9065 domnsymfi
9153 sdomdomtrfi
9154 domsdomtrfi
9155 sucdom2
9156 php3
9162 1sdom2dom
9197 sucxpdom
9205 findcard3
9235 isfinite2
9251 pwfiOLD
9297 card2on
9498 fict
9597 fidomtri2
9938 prdom2
9950 infxpenlem
9957 indcardi
9985 alephnbtwn2
10016 alephsucdom
10023 alephdom
10025 dfac13
10086 djulepw
10136 infdjuabs
10150 infdif
10153 infunsdom1
10157 infunsdom
10158 infxp
10159 cfslb2n
10212 sdom2en01
10246 isfin32i
10309 fin34
10334 fin67
10339 hsmexlem1
10370 hsmex3
10378 entri3
10503 alephexp1
10523 gchdomtri
10573 canthp1
10598 pwfseqlem5
10607 gchdjuidm
10612 gchxpidm
10613 gchpwdom
10614 hargch
10617 gchaclem
10622 gchhar
10623 gchac
10625 inawinalem
10633 inar1
10719 rankcf
10721 tskuni
10727 grothac
10774 rpnnen
16117 rexpen
16118 aleph1irr
16136 dis1stc
22873 hauspwdom
22875 sibfof
33004 ctbssinf
35927 pibt2
35938 heiborlem3
36322 harinf
41405 saluncl
44648 meadjun
44793 meaiunlelem
44799 omeunle
44847 |