Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 Vcvv 3448
suc csuc 6324 |
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 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 ax-un 7677 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-sn 4592 df-pr 4594 df-uni 4871 df-suc 6328 |
This theorem is referenced by: orduninsuc
7784 tfindsg
7802 tfinds2
7805 finds
7840 findsg
7841 finds2
7842 seqomlem1
8401 2oexOLD
8438 oasuc
8475 onasuc
8479 naddcllem
8627 infensuc
9106 phplem4OLD
9171 phpOLD
9173 inf0
9564 inf3lem1
9571 dfom3
9590 cantnflt
9615 cantnflem1
9632 cnfcom
9643 brttrcl2
9657 ssttrcl
9658 ttrcltr
9659 ttrclss
9663 ttrclselem2
9669 infxpenlem
9956 pwsdompw
10147 cfslb2n
10211 cfsmolem
10213 fin1a2lem12
10354 axdc4lem
10398 alephreg
10525 bnj986
33607 bnj1018g
33615 bnj1018
33616 satf
33987 dfon2lem7
34403 rdgssun
35878 dford3lem2
41380 |