Theorem elong 6315

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  Ord word 6306  Oncon0 6307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3438  df-ss 3920  df-uni 4859  df-tr 5200  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310  df-on 6311

This theorem is referenced by:  elon  6316  eloni  6317  elon2  6318  ordelon  6331  onin  6338  limelon  6372  ordsssuc2  6400  onprc  7714  ssonuni  7716  sucexeloni  7745  cofon1  8590  cofon2  8591  enp1i  9168  oion  9428  hartogs  9436  card2on  9446  tskwe  9846  onssnum  9934  hsmexlem1  10320  ondomon  10457  1stcrestlem  23337  nosupno  27613  noinfno  27628  hfninf  36170  rn1st  45261