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

Theorem elong 5874
 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.
StepHypRef Expression
1 ordeq 5873 . 2 (𝑥 = 𝐴 → (Ord 𝑥 ↔ Ord 𝐴))
2 df-on 5870 . 2 On = {𝑥 ∣ Ord 𝑥}
31, 2elab2g 3502 1 (𝐴𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∈ wcel 2144  Ord word 5865  Oncon0 5866 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-v 3351  df-in 3728  df-ss 3735  df-uni 4573  df-tr 4885  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-ord 5869  df-on 5870 This theorem is referenced by:  elon  5875  eloni  5876  elon2  5877  ordelon  5890  onin  5897  limelon  5931  ordsssuc2  5957  onprc  7130  ssonuni  7132  suceloni  7159  ordsuc  7160  oion  8596  hartogs  8604  card2on  8614  tskwe  8975  onssnum  9062  hsmexlem1  9449  ondomon  9586  1stcrestlem  21475  nosupno  32180  hfninf  32624
 Copyright terms: Public domain W3C validator