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

Theorem onelss 6426
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 6394 . 2 (𝐴 ∈ On → Ord 𝐴)
2 ordelss 6400 . . 3 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
32ex 412 . 2 (Ord 𝐴 → (𝐵𝐴𝐵𝐴))
41, 3syl 17 1 (𝐴 ∈ On → (𝐵𝐴𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  wss 3951  Ord word 6383  Oncon0 6384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-ss 3968  df-uni 4908  df-tr 5260  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388
This theorem is referenced by:  ordunidif  6433  onelssi  6499  ssorduni  7799  sucexeloniOLD  7830  suceloniOLD  7832  tfisi  7880  poseq  8183  tfrlem9  8425  tfrlem11  8428  oaordex  8596  oaass  8599  odi  8617  omass  8618  oewordri  8630  nnaordex  8676  domtriord  9163  hartogs  9584  card2on  9594  tskwe  9990  infxpenlem  10053  cfub  10289  cfsuc  10297  coflim  10301  hsmexlem2  10467  ondomon  10603  pwcfsdom  10623  inar1  10815  tskord  10820  grudomon  10857  gruina  10858  sltres  27707  nosupno  27748  nosupbday  27750  noinfno  27763  oldssmade  27916  madebday  27938  mulsproplem13  28154  mulsproplem14  28155  dfrdg2  35796  aomclem6  43071  nnoeomeqom  43325  naddgeoa  43407  naddwordnexlem1  43410  naddwordnexlem4  43414  iscard5  43549
  Copyright terms: Public domain W3C validator