Theorem elong 6331

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  Ord word 6322  Oncon0 6323

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3431  df-ss 3906  df-uni 4851  df-tr 5193  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327

This theorem is referenced by:  elon  6332  eloni  6333  elon2  6334  ordelon  6347  onin  6354  limelon  6388  ordsssuc2  6416  onprc  7732  ssonuni  7734  sucexeloni  7763  cofon1  8608  cofon2  8609  enp1i  9189  oion  9451  hartogs  9459  card2on  9469  tskwe  9874  onssnum  9962  hsmexlem1  10348  ondomon  10485  1stcrestlem  23417  nosupno  27667  noinfno  27682  hfninf  36368  rn1st  45702