Theorem elong 6369

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-v 3455  df-ss 3919  df-uni 4871  df-tr 5217  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365

This theorem is used by:  elon  6370  eloni  6371  elon2  6372  ordelon  6385  onin  6393  limelon  6427  ordsssuc2  6455  onprc  7780  ssonuni  7782  sucexeloni  7811  cofon1  8663  cofon2  8664  enp1i  9252  oion  9511  hartogs  9519  card2on  9529  tskwe  9958  onssnum  10046  hsmexlem1  10431  ondomon  10574  1stcrestlem  23678  nosupno  27937  noinfno  27952  hfninf  36753  rn1st  46089