Theorem onsucb 7761

Description: A class is an ordinal number if and only if its successor is an ordinal number. Biconditional form of onsuc 7757. (Contributed by NM, 9-Sep-2003.)

Assertion

Ref	Expression
onsucb	⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)

Proof of Theorem onsucb

Step	Hyp	Ref	Expression
1		ordsuc 7758	. . 3 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
2		sucexb 7751	. . 3 ⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
3	1, 2	anbi12i 629	. 2 ⊢ ((Ord 𝐴 ∧ 𝐴 ∈ V) ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
4		elon2 6328	. 2 ⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
5		elon2 6328	. 2 ⊢ (suc 𝐴 ∈ On ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
6	3, 4, 5	3bitr4i 303	1 ⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  Vcvv 3430  Ord word 6316  Oncon0 6317  suc csuc 6319

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-ord 6320  df-on 6321  df-suc 6323

This theorem is referenced by:  onsucmin  7765  tfindsg2  7806  oaordi  8474  oalimcl  8488  omlimcl  8506  omeulem1  8510  oeordsuc  8523  naddcllem  8605  infensuc  9086  cantnflem1b  9598  cantnflem1  9601  r1ordg  9693  alephnbtwn  9984  cfsuc  10170  alephsuc3  10494  alephreg  10496  bdayimaon  27671  nosupbnd1lem1  27686  nosupbnd1  27692  nosupbnd2lem1  27693  nosupbnd2  27694  noinfno  27696  noinfres  27700  noinfbnd1lem1  27701  noinfbnd1  27707  noinfbnd2lem1  27708  noinfbnd2  27709  noeta2  27767  etaslts2  27800