Theorem elong 6356

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2144  Ord word 6347  Oncon0 6348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-v 3458  df-ss 3923  df-uni 4868  df-tr 5210  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-ord 6351  df-on 6352

This theorem is referenced by:  elon  6357  eloni  6358  elon2  6359  ordelon  6372  onin  6379  limelon  6413  ordsssuc2  6441  onprc  7763  ssonuni  7765  sucexeloni  7794  cofon1  8644  cofon2  8645  enp1i  9225  oion  9486  hartogs  9494  card2on  9504  tskwe  9910  onssnum  9998  hsmexlem1  10385  ondomon  10522  1stcrestlem  23514  nosupno  27769  noinfno  27784  hfninf  36541  rn1st  45853