Theorem peano2b 7893

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 7892	. 2 ⊢ Lim ω
2		limsuc 7859	. 2 ⊢ (Lim ω → (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈ ω)

Syntax hints:   ↔ wb 205   ∈ wcel 2099  Lim wlim 6377  suc csuc 6378  ωcom 7876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433  ax-un 7746

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-tr 5271  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-om 7877

This theorem is referenced by:  nnsuc  7894  peano2  7902  peano5  7905  peano5OLD  7906  frsuc  8467  frsucmptn  8469  nnaordi  8648  nnmsucr  8655  omsmolem  8687  php  9244  php4  9247  phpOLD  9256  unblem1  9329  isfinite2  9335  inf0  9664  inf3lem1  9671  inf3lem5  9675  cantnfp1lem3  9723  cantnflem1  9732  itunisuc  10462  ituniiun  10465  indpi  10950  rdgeqoa  37077