Theorem onsucb 7753

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

Assertion

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

Proof of Theorem onsucb

Step	Hyp	Ref	Expression
1		ordsuc 7750	. . 3 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
2		sucexb 7743	. . 3 ⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
3	1, 2	anbi12i 628	. 2 ⊢ ((Ord 𝐴 ∧ 𝐴 ∈ V) ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
4		elon2 6323	. 2 ⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
5		elon2 6323	. 2 ⊢ (suc 𝐴 ∈ On ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
6	3, 4, 5	3bitr4i 303	1 ⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2111  Vcvv 3436  Ord word 6311  Oncon0 6312  suc csuc 6314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-tr 5201  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6315  df-on 6316  df-suc 6318

This theorem is referenced by:  onsucmin  7757  tfindsg2  7798  oaordi  8467  oalimcl  8481  omlimcl  8499  omeulem1  8503  oeordsuc  8515  naddcllem  8597  infensuc  9074  cantnflem1b  9582  cantnflem1  9585  r1ordg  9677  alephnbtwn  9968  cfsuc  10154  alephsuc3  10477  alephreg  10479  bdayimaon  27638  nosupbnd1lem1  27653  nosupbnd1  27659  nosupbnd2lem1  27660  nosupbnd2  27661  noinfno  27663  noinfres  27667  noinfbnd1lem1  27668  noinfbnd1  27674  noinfbnd2lem1  27675  noinfbnd2  27676  noeta2  27730  etasslt2  27761