Theorem elong 6373

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2107  Ord word 6364  Oncon0 6365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-tr 5267  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369

This theorem is referenced by:  elon  6374  eloni  6375  elon2  6376  ordelon  6389  onin  6396  limelon  6429  ordsssuc2  6456  onprc  7765  ssonuni  7767  sucexeloni  7797  sucexeloniOLD  7798  suceloniOLD  7800  ordsucOLD  7802  cofon1  8671  cofon2  8672  enp1i  9279  oion  9531  hartogs  9539  card2on  9549  tskwe  9945  onssnum  10035  hsmexlem1  10421  ondomon  10558  1stcrestlem  22956  nosupno  27206  noinfno  27221  hfninf  35158  rn1st  43978