Theorem onsucb 7788

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

Assertion

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

Proof of Theorem onsucb

Step	Hyp	Ref	Expression
1		ordsuc 7784	. . 3 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)
2		sucexb 7775	. . 3 ⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V)
3	1, 2	anbi12i 627	. 2 ⊢ ((Ord 𝐴 ∧ 𝐴 ∈ V) ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
4		elon2 6364	. 2 ⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
5		elon2 6364	. 2 ⊢ (suc 𝐴 ∈ On ↔ (Ord suc 𝐴 ∧ suc 𝐴 ∈ V))
6	3, 4, 5	3bitr4i 302	1 ⊢ (𝐴 ∈ On ↔ suc 𝐴 ∈ On)

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  Vcvv 3473  Ord word 6352  Oncon0 6353  suc csuc 6355

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 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7708

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 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-tr 5259  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-ord 6356  df-on 6357  df-suc 6359

This theorem is referenced by:  onsucmin  7792  tfindsg2  7834  oaordi  8529  oalimcl  8543  omlimcl  8561  omeulem1  8565  oeordsuc  8577  naddcllem  8658  infensuc  9138  cantnflem1b  9663  cantnflem1  9666  r1ordg  9755  alephnbtwn  10048  cfsuc  10234  alephsuc3  10557  alephreg  10559  bdayimaon  27123  nosupbnd1lem1  27138  nosupbnd1  27144  nosupbnd2lem1  27145  nosupbnd2  27146  noinfno  27148  noinfres  27152  noinfbnd1lem1  27153  noinfbnd1  27159  noinfbnd2lem1  27160  noinfbnd2  27161  noeta2  27212  etasslt2  27241