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

Theorem snsstp2 4707
 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 4705 . . 3 {𝐵} ⊆ {𝐴, 𝐵}
2 ssun1 4077 . . 3 {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
31, 2sstri 3901 . 2 {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4 df-tp 4527 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
53, 4sseqtrri 3929 1 {𝐵} ⊆ {𝐴, 𝐵, 𝐶}
 Colors of variables: wff setvar class Syntax hints:   ∪ cun 3856   ⊆ wss 3858  {csn 4522  {cpr 4524  {ctp 4526 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 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3863  df-in 3865  df-ss 3875  df-pr 4525  df-tp 4527 This theorem is referenced by:  fr3nr  7493  rngplusg  16679  srngplusg  16687  lmodplusg  16696  ipsaddg  16703  ipsvsca  16706  phlplusg  16713  topgrpplusg  16721  otpstset  16728  odrngplusg  16739  odrngle  16742  prdsplusg  16789  prdsvsca  16791  prdsle  16793  imasplusg  16848  imasvsca  16851  imasle  16854  fuchom  17290  setchomfval  17405  catchomfval  17424  estrchomfval  17442  xpchomfval  17495  cnfldadd  20171  cnfldle  20175  psrplusg  20709  psrvscafval  20718  trkgdist  26339  idlsrgplusg  31171  algaddg  40496  clsk1indlem4  41120  rngchomfvalALTV  44975  ringchomfvalALTV  45038
 Copyright terms: Public domain W3C validator