Theorem elong 5731

Description: An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
elong	|- ( A e. V -> ( A e. On <-> Ord A ) )

Proof of Theorem elong

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ordeq 5730	. 2 |- ( x = A -> ( Ord x <-> Ord A ) )
2		df-on 5727	. 2 |- On = { x | Ord x }
3	1, 2	elab2g 3353	1 |- ( A e. V -> ( A e. On <-> Ord A ) )

Syntax hints:   -> wi 4   <-> wb 196   e. wcel 1990   Ord word 5722   Oncon0 5723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-uni 4437  df-tr 4753  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726  df-on 5727

This theorem is referenced by:  elon  5732  eloni  5733  elon2  5734  ordelon  5747  onin  5754  limelon  5788  ordsssuc2  5814  onprc  6984  ssonuni  6986  suceloni  7013  ordsuc  7014  oion  8441  hartogs  8449  card2on  8459  tskwe  8776  onssnum  8863  hsmexlem1  9248  ondomon  9385  1stcrestlem  21255  nosupno  31849  hfninf  32293