Theorem elong 6304

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 6303	. 2 ⊢ (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴))
2		df-on 6300	. 2 ⊢ On = {𝑥 ∣ Ord 𝑥}
3	1, 2	elab2g 3621	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2105  Ord word 6295  Oncon0 6296

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-v 3443  df-in 3904  df-ss 3914  df-uni 4852  df-tr 5207  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-ord 6299  df-on 6300

This theorem is referenced by:  elon  6305  eloni  6306  elon2  6307  ordelon  6320  onin  6327  limelon  6359  ordsssuc2  6386  onprc  7682  ssonuni  7684  sucexeloni  7714  sucexeloniOLD  7715  suceloniOLD  7717  ordsucOLD  7719  enp1i  9136  oion  9385  hartogs  9393  card2on  9403  tskwe  9799  onssnum  9889  hsmexlem1  10275  ondomon  10412  1stcrestlem  22701  nosupno  26949  noinfno  26964  hfninf  34579