Theorem elong 6403

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  Ord word 6394  Oncon0 6395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-ss 3993  df-uni 4932  df-tr 5284  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-ord 6398  df-on 6399

This theorem is referenced by:  elon  6404  eloni  6405  elon2  6406  ordelon  6419  onin  6426  limelon  6459  ordsssuc2  6486  onprc  7813  ssonuni  7815  sucexeloni  7845  sucexeloniOLD  7846  suceloniOLD  7848  ordsucOLD  7850  cofon1  8728  cofon2  8729  enp1i  9341  oion  9605  hartogs  9613  card2on  9623  tskwe  10019  onssnum  10109  hsmexlem1  10495  ondomon  10632  1stcrestlem  23481  nosupno  27766  noinfno  27781  hfninf  36150  rn1st  45183