Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
class class class wbr 5106 dom cdm 5634
Oncon0 6318 ≈ cen 8883
cardccrd 9876 |
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 5257 ax-nul 5264 ax-pow 5321 ax-pr 5385 ax-un 7673 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3or 1089 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-ne 2941 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3930 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-int 4909 df-br 5107 df-opab 5169 df-mpt 5190 df-tr 5224 df-id 5532 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5589 df-we 5591 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-ord 6321 df-on 6322 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 df-en 8887 df-card 9880 |
This theorem is referenced by: oncardval
9896 oncardid
9897 cardnn
9904 iscard
9916 carduni
9922 nnsdomel
9931 harsdom
9936 harsucnn
9939 pm54.43lem
9941 infxpenlem
9954 infxpidm2
9958 onssnum
9981 alephnbtwn
10012 alephnbtwn2
10013 alephordilem1
10014 alephord2
10017 alephsdom
10027 cardaleph
10030 infenaleph
10032 alephinit
10036 iunfictbso
10055 ficardun2
10143 ficardun2OLD
10144 pwsdompw
10145 infunsdom1
10154 ackbij2
10184 cfflb
10200 sdom2en01
10243 fin23lem22
10268 iunctb
10515 alephadd
10518 alephmul
10519 alephexp1
10520 alephsuc3
10521 canthp1lem2
10594 pwfseqlem4a
10602 pwfseqlem4
10603 pwfseqlem5
10604 gchaleph
10612 gchaleph2
10613 hargch
10614 cygctb
19674 ttac
41403 numinfctb
41473 isnumbasgrplem2
41474 isnumbasabl
41476 iscard4
41893 minregex2
41895 harval3
41898 harval3on
41899 aleph1min
41917 |