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

Theorem onelss 5909
Description: An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
onelss (𝐴 ∈ On → (𝐵𝐴𝐵𝐴))

Proof of Theorem onelss
StepHypRef Expression
1 eloni 5876 . 2 (𝐴 ∈ On → Ord 𝐴)
2 ordelss 5882 . . 3 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
32ex 397 . 2 (Ord 𝐴 → (𝐵𝐴𝐵𝐴))
41, 3syl 17 1 (𝐴 ∈ On → (𝐵𝐴𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  wss 3723  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 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-v 3353  df-in 3730  df-ss 3737  df-uni 4575  df-tr 4887  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-ord 5869  df-on 5870
This theorem is referenced by:  ordunidif  5916  onelssi  5979  ssorduni  7132  suceloni  7160  tfisi  7205  tfrlem9  7634  tfrlem11  7637  oaordex  7792  oaass  7795  odi  7813  omass  7814  oewordri  7826  nnaordex  7872  domtriord  8262  hartogs  8605  card2on  8615  tskwe  8976  infxpenlem  9036  cfub  9273  cfsuc  9281  coflim  9285  hsmexlem2  9451  ondomon  9587  pwcfsdom  9607  inar1  9799  tskord  9804  grudomon  9841  gruina  9842  dfrdg2  32037  poseq  32090  sltres  32152  nosupno  32186  aomclem6  38155
  Copyright terms: Public domain W3C validator