Theorem elong 6343

Description: An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
elong	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))

Proof of Theorem elong

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ordeq 6342	. 2 ⊢ (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴))
2		df-on 6339	. 2 ⊢ On = {𝑥 ∣ Ord 𝑥}
3	1, 2	elab2g 3650	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  Ord word 6334  Oncon0 6335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3452  df-ss 3934  df-uni 4875  df-tr 5218  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339

This theorem is referenced by:  elon  6344  eloni  6345  elon2  6346  ordelon  6359  onin  6366  limelon  6400  ordsssuc2  6428  onprc  7757  ssonuni  7759  sucexeloni  7788  sucexeloniOLD  7789  ordsucOLD  7792  cofon1  8639  cofon2  8640  enp1i  9231  oion  9496  hartogs  9504  card2on  9514  tskwe  9910  onssnum  10000  hsmexlem1  10386  ondomon  10523  1stcrestlem  23346  nosupno  27622  noinfno  27637  hfninf  36181  rn1st  45274