Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
Ord word 6364 Oncon0 6365
ωcom 7855 |
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-ral 3063 df-rab 3434 df-v 3477 df-in 3956 df-ss 3966 df-uni 4910 df-tr 5267 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-ord 6368 df-on 6369 df-om 7856 |
This theorem is referenced by: nnlim
7869 nnsuc
7873 omsucne
7874 omun
7878 nnaordi
8618 nnaord
8619 nnaword
8627 nnmord
8632 nnmwordi
8635 nnawordex
8637 omsmo
8657 eldifsucnn
8663 enrefnn
9047 dif1enlemOLD
9157 pssnn
9168 unfi
9172 phplem2
9208 php
9210 php4
9213 nndomog
9216 phplem1OLD
9217 phplem2OLD
9218 phplem3OLD
9219 phplem4OLD
9220 phpOLD
9222 nndomogOLD
9226 onomeneq
9228 ominf
9258 ominfOLD
9259 isinf
9260 isinfOLD
9261 pssnnOLD
9265 dif1ennnALT
9277 findcard3
9285 unblem1
9295 isfinite2
9301 unfilem1
9310 inf3lem5
9627 inf3lem6
9628 cantnfp1lem2
9674 cantnfp1lem3
9675 ttrcltr
9711 ttrclss
9715 dmttrcl
9716 rnttrcl
9717 ttrclselem2
9721 dif1card
10005 nnadju
10192 pwsdompw
10199 ackbij1lem5
10219 ackbij1lem14
10228 ackbij1lem16
10230 ackbij1b
10234 ackbij2
10238 sornom
10272 infpssrlem4
10301 infpssrlem5
10302 fin23lem26
10320 fin23lem23
10321 isf32lem2
10349 isf32lem3
10350 isf32lem4
10351 domtriomlem
10437 axdc3lem2
10446 axdc3lem4
10448 canthp1lem2
10648 elni2
10872 piord
10875 addnidpi
10896 indpi
10902 om2uzf1oi
13918 fzennn
13933 hashp1i
14363 bnj529
33752 bnj1098
33794 bnj570
33916 bnj594
33923 bnj580
33924 bnj967
33956 bnj1001
33970 bnj1053
33987 bnj1071
33988 nnuni
34696 hfun
35150 finminlem
35203 finxpsuclem
36278 finxpsuc
36279 wepwso
41785 dflim5
42079 |