Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
Ord word 6317 Oncon0 6318
ωcom 7803 |
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 3062 df-rab 3407 df-v 3446 df-in 3918 df-ss 3928 df-uni 4867 df-tr 5224 df-po 5546 df-so 5547 df-fr 5589 df-we 5591 df-ord 6321 df-on 6322 df-om 7804 |
This theorem is referenced by: nnlim
7817 nnsuc
7821 omsucne
7822 nnaordi
8566 nnaord
8567 nnaword
8575 nnmord
8580 nnmwordi
8583 nnawordex
8585 omsmo
8605 eldifsucnn
8611 enrefnn
8994 dif1enlemOLD
9104 pssnn
9115 unfi
9119 phplem2
9155 php
9157 php4
9160 nndomog
9163 phplem1OLD
9164 phplem2OLD
9165 phplem3OLD
9166 phplem4OLD
9167 phpOLD
9169 nndomogOLD
9173 onomeneq
9175 ominf
9205 ominfOLD
9206 isinf
9207 isinfOLD
9208 pssnnOLD
9212 dif1ennnALT
9224 findcard3
9232 unblem1
9242 isfinite2
9248 unfilem1
9257 inf3lem5
9573 inf3lem6
9574 cantnfp1lem2
9620 cantnfp1lem3
9621 ttrcltr
9657 ttrclss
9661 dmttrcl
9662 rnttrcl
9663 ttrclselem2
9667 dif1card
9951 nnadju
10138 pwsdompw
10145 ackbij1lem5
10165 ackbij1lem14
10174 ackbij1lem16
10176 ackbij1b
10180 ackbij2
10184 sornom
10218 infpssrlem4
10247 infpssrlem5
10248 fin23lem26
10266 fin23lem23
10267 isf32lem2
10295 isf32lem3
10296 isf32lem4
10297 domtriomlem
10383 axdc3lem2
10392 axdc3lem4
10394 canthp1lem2
10594 elni2
10818 piord
10821 addnidpi
10842 indpi
10848 om2uzf1oi
13864 fzennn
13879 hashp1i
14309 bnj529
33410 bnj1098
33452 bnj570
33574 bnj594
33581 bnj580
33582 bnj967
33614 bnj1001
33628 bnj1053
33645 bnj1071
33646 nnuni
34355 hfun
34809 finminlem
34836 finxpsuclem
35914 finxpsuc
35915 wepwso
41413 dflim5
41707 |