Theorem elong 6322

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  Ord word 6313  Oncon0 6314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3050  df-v 3440  df-ss 3916  df-uni 4861  df-tr 5203  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318

This theorem is referenced by:  elon  6323  eloni  6324  elon2  6325  ordelon  6338  onin  6345  limelon  6379  ordsssuc2  6407  onprc  7720  ssonuni  7722  sucexeloni  7751  cofon1  8596  cofon2  8597  enp1i  9173  oion  9432  hartogs  9440  card2on  9450  tskwe  9853  onssnum  9941  hsmexlem1  10327  ondomon  10464  1stcrestlem  23377  nosupno  27652  noinfno  27667  hfninf  36241  rn1st  45384