Theorem peano2b 7895

Description: A class belongs to omega iff its successor does. (Contributed by NM, 3-Dec-1995.)

Assertion

Ref	Expression
peano2b	⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)

Proof of Theorem peano2b

Step	Hyp	Ref	Expression
1		limom 7894	. 2 ⊢ Lim ω
2		limsuc 7861	. 2 ⊢ (Lim ω → (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144  Lim wlim 6363  suc csuc 6364  ωcom 7878

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-om 7879

This theorem is used by:  nnsuc  7896  peano2  7902  peano5  7906  frsuc  8449  frsucmptn  8451  nnaordi  8631  nnmsucr  8638  omsmolem  8670  php  9226  php4  9229  unblem1  9288  isfinite2  9294  inf0  9626  inf3lem1  9633  inf3lem5  9637  cantnfp1lem3  9685  cantnflem1  9694  itunisuc  10501  ituniiun  10504  indpi  10996  constrllcllem  34431  constrlccllem  34432  constrcccllem  34433  mh-inf3f1  37422  rdgeqoa  38387