Theorem elong 6327

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  Ord word 6318  Oncon0 6319

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3432  df-ss 3907  df-uni 4852  df-tr 5194  df-po 5534  df-so 5535  df-fr 5579  df-we 5581  df-ord 6322  df-on 6323

This theorem is referenced by:  elon  6328  eloni  6329  elon2  6330  ordelon  6343  onin  6350  limelon  6384  ordsssuc2  6412  onprc  7727  ssonuni  7729  sucexeloni  7758  cofon1  8603  cofon2  8604  enp1i  9184  oion  9446  hartogs  9454  card2on  9464  tskwe  9869  onssnum  9957  hsmexlem1  10343  ondomon  10480  1stcrestlem  23431  nosupno  27685  noinfno  27700  hfninf  36388  rn1st  45724