Colors of
variables: wff
setvar class |
Syntax hints:
∪ cun 3947 ⊆ wss 3949
{csn 4629 suc csuc 6367 |
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-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3954 df-in 3956 df-ss 3966 df-suc 6371 |
This theorem is referenced by: trsuc
6452 sucexeloniOLD
7798 suceloniOLD
7800 limsssuc
7839 oaordi
8546 omeulem1
8582 oelim2
8595 nnaordi
8618 naddcllem
8675 phplem2
9208 php
9210 phplem4OLD
9220 phpOLD
9222 onomeneqOLD
9229 enp1i
9279 fiint
9324 cantnfval2
9664 cantnfle
9666 cantnfp1lem3
9675 cnfcomlem
9694 ttrclss
9715 ranksuc
9860 fseqenlem1
10019 pwsdompw
10199 fin1a2lem12
10406 canthp1lem2
10648 nosupbnd1
27217 nosupbnd2lem1
27218 noinfbnd1
27232 noinfbnd2lem1
27233 satfvsucsuc
34387 satffunlem2lem2
34428 satffunlem2
34430 limsucncmpi
35378 finxpreclem3
36322 insucid
42202 minregex
42333 clsk1independent
42845 grur1cld
43039 suctrALT
43635 suctrALT2VD
43645 suctrALT2
43646 suctrALTcf
43731 suctrALTcfVD
43732 suctrALT3
43733 |