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

Theorem snsstp2 4777
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 4775 . . 3 {𝐵} ⊆ {𝐴, 𝐵}
2 ssun1 4137 . . 3 {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
31, 2sstri 3953 . 2 {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4 df-tp 4590 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
53, 4sseqtrri 3993 1 {𝐵} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3909  wss 3911  {csn 4585  {cpr 4587  {ctp 4589
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 2008  ax-8 2111  ax-9 2119  ax-ext 2701
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-ss 3928  df-pr 4588  df-tp 4590
This theorem is referenced by:  fr3nr  7728  rngplusg  17239  srngplusg  17250  lmodplusg  17266  ipsaddg  17277  ipsvsca  17280  phlplusg  17287  topgrpplusg  17302  otpstset  17317  odrngplusg  17344  odrngle  17347  prdsplusg  17397  prdsvsca  17399  prdsle  17401  imasplusg  17456  imasvsca  17459  imasle  17462  fuchom  17906  setchomfval  18021  catchomfval  18044  estrchomfval  18067  xpchomfval  18120  mpocnfldadd  21301  cnfldle  21307  cnfldaddOLD  21316  cnfldleOLD  21320  psrplusg  21878  psrvscafval  21890  trkgdist  28426  rlocaddval  33235  idlsrgplusg  33469  algaddg  43157  clsk1indlem4  44026  rngchomfvalALTV  48248  ringchomfvalALTV  48282  cathomfval  49209  mndtchom  49566
  Copyright terms: Public domain W3C validator