| Colors of
variables: wff
setvar class |
| Syntax hints:
→ wi 4 ∧ wa 396
∈ wcel 2106 ⊆
wss 3941 class class class wbr 5138
dom cdm 5666 ≼ cdom 8917
cardccrd 9909 |
| 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 2702 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7705 |
| This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3430 df-v 3472 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-pss 3960 df-nul 4316 df-if 4520 df-pw 4595 df-sn 4620 df-pr 4622 df-op 4626 df-uni 4899 df-int 4941 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-se 5622 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6286 df-ord 6353 df-on 6354 df-suc 6356 df-iota 6481 df-fun 6531 df-fn 6532 df-f 6533 df-f1 6534 df-fo 6535 df-f1o 6536 df-fv 6537 df-isom 6538 df-riota 7346 df-ov 7393 df-2nd 7955 df-frecs 8245 df-wrecs 8276 df-recs 8350 df-er 8683 df-en 8920 df-dom 8921 df-card 9913 |
| This theorem is referenced by: onssnum
10014 numacn
10023 dfac12r
10120 infdif
10183 fin23lem22
10301 ttukey2g
10490 smobeth
10560 canthnumlem
10622 gchac
10655 tskurn
10763 lbsextlem4
20718 1stcrestlem
22880 2ndcsep
22887 filssufilg
23339 ptcmplem2
23481 ptcmplem3
23482 poimirlem32
36308 ttac
41532 rn1st
43737 |
