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

Theorem snsstp2 4742
Description: A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
Assertion
Ref Expression
snsstp2 {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Proof of Theorem snsstp2
StepHypRef Expression
1 snsspr2 4740 . . 3 {𝐵} ⊆ {𝐴, 𝐵}
2 ssun1 4145 . . 3 {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
31, 2sstri 3973 . 2 {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4 df-tp 4562 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
53, 4sseqtrri 4001 1 {𝐵} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3931  wss 3933  {csn 4557  {cpr 4559  {ctp 4561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-in 3940  df-ss 3949  df-pr 4560  df-tp 4562
This theorem is referenced by:  fr3nr  7483  rngplusg  16609  srngplusg  16617  lmodplusg  16626  ipsaddg  16633  ipsvsca  16636  phlplusg  16643  topgrpplusg  16651  otpstset  16658  odrngplusg  16669  odrngle  16672  prdsplusg  16719  prdsvsca  16721  prdsle  16723  imasplusg  16778  imasvsca  16781  imasle  16784  fuchom  17219  setchomfval  17327  catchomfval  17346  estrchomfval  17364  xpchomfval  17417  psrplusg  20089  psrvscafval  20098  cnfldadd  20478  cnfldle  20482  trkgdist  26159  algaddg  39657  clsk1indlem4  40272  rngchomfvalALTV  44183  ringchomfvalALTV  44246
  Copyright terms: Public domain W3C validator