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

Theorem onelss 5735
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 5702 . 2 (𝐴 ∈ On → Ord 𝐴)
2 ordelss 5708 . . 3 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
32ex 450 . 2 (Ord 𝐴 → (𝐵𝐴𝐵𝐴))
41, 3syl 17 1 (𝐴 ∈ On → (𝐵𝐴𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  wss 3560  Ord word 5691  Oncon0 5692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-v 3192  df-in 3567  df-ss 3574  df-uni 4410  df-tr 4723  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-ord 5695  df-on 5696
This theorem is referenced by:  ordunidif  5742  onelssi  5805  ssorduni  6947  suceloni  6975  tfisi  7020  tfrlem9  7441  tfrlem11  7444  oaordex  7598  oaass  7601  odi  7619  omass  7620  oewordri  7632  nnaordex  7678  domtriord  8066  hartogs  8409  card2on  8419  tskwe  8736  infxpenlem  8796  cfub  9031  cfsuc  9039  coflim  9043  hsmexlem2  9209  ondomon  9345  pwcfsdom  9365  inar1  9557  tskord  9562  grudomon  9599  gruina  9600  dfrdg2  31455  poseq  31504  sltres  31571  nobndup  31616  nobnddown  31617  aomclem6  37148
  Copyright terms: Public domain W3C validator