Theorem elong 6360

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145  Ord word 6351  Oncon0 6352

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3916  df-uni 4868  df-tr 5213  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-ord 6355  df-on 6356

This theorem is used by:  elon  6361  eloni  6362  elon2  6363  ordelon  6376  onin  6384  limelon  6418  ordsssuc2  6446  onprc  7776  ssonuni  7778  sucexeloni  7807  cofon1  8660  cofon2  8661  enp1i  9249  oion  9508  hartogs  9516  card2on  9526  tskwe  9988  onssnum  10076  hsmexlem1  10461  ondomon  10604  1stcrestlem  23717  nosupno  27979  noinfno  27994  hfninf  36851  rn1st  46200