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  17902  setchomfval  18017  catchomfval  18040  estrchomfval  18063  xpchomfval  18116  mpocnfldadd  21245  cnfldle  21251  cnfldaddOLD  21260  cnfldleOLD  21264  psrplusg  21821  psrvscafval  21833  trkgdist  28349  rlocaddval  33192  idlsrgplusg  33449  algaddg  43137  clsk1indlem4  44006  rngchomfvalALTV  48228  ringchomfvalALTV  48262  cathomfval  49189  mndtchom  49546
  Copyright terms: Public domain W3C validator