Theorem elong 6368

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2142  Ord word 6359  Oncon0 6360

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-v 3456  df-ss 3921  df-uni 4872  df-tr 5218  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-ord 6363  df-on 6364

This theorem is used by:  elon  6369  eloni  6370  elon2  6371  ordelon  6384  onin  6392  limelon  6426  ordsssuc2  6454  onprc  7775  ssonuni  7777  sucexeloni  7806  cofon1  8656  cofon2  8657  enp1i  9237  oion  9496  hartogs  9504  card2on  9514  tskwe  9943  onssnum  10031  hsmexlem1  10416  ondomon  10553  1stcrestlem  23620  nosupno  27878  noinfno  27893  hfninf  36686  rn1st  46016