Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2106
suc csuc 6366 ωcom 7857 |
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-ext 2703 ax-sep 5299 ax-nul 5306 ax-pr 5427 ax-un 7727 |
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-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-tr 5266 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-om 7858 |
This theorem is referenced by: onnseq
8346 seqomlem1
8452 seqomlem4
8455 onasuc
8530 onmsuc
8531 onesuc
8532 o2p2e4
8543 nnacl
8613 nnecl
8615 nnacom
8619 nnmsucr
8627 1onnALT
8642 2onnALT
8644 3onn
8645 4onn
8646 nnneo
8656 nneob
8657 omopthlem1
8660 eldifsucnn
8665 findcard
9165 unfi
9174 phplem1
9209 php
9212 onomeneqOLD
9231 dif1ennnALT
9279 findcard2OLD
9286 unbnn2
9302 dffi3
9428 wofib
9542 axinf2
9637 dfom3
9644 noinfep
9657 cantnflt
9669 ttrcltr
9713 ttrclss
9717 ttrclselem2
9723 trcl
9725 cardsucnn
9982 harsucnn
9995 dif1card
10007 fseqdom
10023 alephfp
10105 ackbij1lem5
10221 ackbij1lem16
10232 ackbij2lem2
10237 ackbij2lem3
10238 ackbij2
10240 sornom
10274 infpssrlem4
10303 fin23lem26
10322 fin23lem20
10334 fin23lem38
10346 fin23lem39
10347 isf32lem2
10351 isf32lem3
10352 isf34lem7
10376 isf34lem6
10377 fin1a2lem6
10402 fin1a2lem9
10405 fin1a2lem12
10408 domtriomlem
10439 axdc2lem
10445 axdc3lem
10447 axdc3lem2
10448 axdc3lem4
10450 axdc4lem
10452 axdclem2
10517 peano2nn
12228 om2uzrani
13921 uzrdgsuci
13929 fzennn
13937 axdc4uzlem
13952 precsexlem4
27883 precsexlem5
27884 precsexlem11
27890 peano2n0s
27928 bnj970
34244 satfvsuc
34638 satfvsucsuc
34642 gonarlem
34671 goalrlem
34673 satffunlem2lem2
34683 satffunlem2
34685 ex-sategoelelomsuc
34703 elhf2
35439 0hf
35441 hfsn
35443 hfpw
35449 neibastop2lem
35548 exrecfnlem
36563 finxpsuclem
36581 domalom
36588 onexoegt
42295 nnoeomeqom
42364 nna1iscard
42598 |