Theorem elong 6379

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2098  Ord word 6370  Oncon0 6371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-v 3463  df-ss 3961  df-uni 4910  df-tr 5267  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-ord 6374  df-on 6375

This theorem is referenced by:  elon  6380  eloni  6381  elon2  6382  ordelon  6395  onin  6402  limelon  6435  ordsssuc2  6462  onprc  7781  ssonuni  7783  sucexeloni  7813  sucexeloniOLD  7814  suceloniOLD  7816  ordsucOLD  7818  cofon1  8693  cofon2  8694  enp1i  9304  oion  9561  hartogs  9569  card2on  9579  tskwe  9975  onssnum  10065  hsmexlem1  10451  ondomon  10588  1stcrestlem  23400  nosupno  27682  noinfno  27697  hfninf  35913  rn1st  44788