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 3659	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  Ord word 6351  Oncon0 6352

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-v 3461  df-ss 3943  df-uni 4884  df-tr 5230  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-on 6356

This theorem is referenced by:  elon  6361  eloni  6362  elon2  6363  ordelon  6376  onin  6383  limelon  6417  ordsssuc2  6444  onprc  7770  ssonuni  7772  sucexeloni  7801  sucexeloniOLD  7802  suceloniOLD  7804  ordsucOLD  7806  cofon1  8682  cofon2  8683  enp1i  9283  oion  9548  hartogs  9556  card2on  9566  tskwe  9962  onssnum  10052  hsmexlem1  10438  ondomon  10575  1stcrestlem  23388  nosupno  27665  noinfno  27680  hfninf  36150  rn1st  45245