MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elong Structured version   Unicode version

Theorem elong 5418
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.
StepHypRef Expression
1 ordeq 5417 . 2  |-  ( x  =  A  ->  ( Ord  x  <->  Ord  A ) )
2 df-on 5414 . 2  |-  On  =  { x  |  Ord  x }
31, 2elab2g 3198 1  |-  ( A  e.  V  ->  ( A  e.  On  <->  Ord  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1842   Ord word 5409   Oncon0 5410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-rex 2760  df-v 3061  df-in 3421  df-ss 3428  df-uni 4192  df-tr 4490  df-po 4744  df-so 4745  df-fr 4782  df-we 4784  df-ord 5413  df-on 5414
This theorem is referenced by:  elon  5419  eloni  5420  elon2  5421  ordelon  5434  onin  5441  limelon  5473  ordsssuc2  5498  onprc  6602  ssonuni  6604  suceloni  6631  ordsuc  6632  oion  7995  hartogs  8003  card2on  8014  tskwe  8363  onssnum  8453  hsmexlem1  8838  ondomon  8970  1stcrestlem  20245  hfninf  30524
  Copyright terms: Public domain W3C validator