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

Theorem onelss 6205
 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 6173 . 2 (𝐴 ∈ On → Ord 𝐴)
2 ordelss 6179 . . 3 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
32ex 416 . 2 (Ord 𝐴 → (𝐵𝐴𝐵𝐴))
41, 3syl 17 1 (𝐴 ∈ On → (𝐵𝐴𝐵𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2112   ⊆ wss 3884  Ord word 6162  Oncon0 6163 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-11 2159  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ral 3114  df-v 3446  df-in 3891  df-ss 3901  df-uni 4804  df-tr 5140  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-ord 6166  df-on 6167 This theorem is referenced by:  ordunidif  6211  onelssi  6271  ssorduni  7484  suceloni  7512  tfisi  7557  tfrlem9  8008  tfrlem11  8011  oaordex  8171  oaass  8174  odi  8192  omass  8193  oewordri  8205  nnaordex  8251  domtriord  8651  hartogs  8996  card2on  9006  tskwe  9367  infxpenlem  9428  cfub  9664  cfsuc  9672  coflim  9676  hsmexlem2  9842  ondomon  9978  pwcfsdom  9998  inar1  10190  tskord  10195  grudomon  10232  gruina  10233  dfrdg2  33148  poseq  33203  sltres  33277  nosupno  33311  aomclem6  39990  iscard5  40229
 Copyright terms: Public domain W3C validator