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

Theorem snsstp2 4483
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 4481 . . 3 {𝐵} ⊆ {𝐴, 𝐵}
2 ssun1 3927 . . 3 {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
31, 2sstri 3761 . 2 {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4 df-tp 4321 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
53, 4sseqtr4i 3787 1 {𝐵} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3721  wss 3723  {csn 4316  {cpr 4318  {ctp 4320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-in 3730  df-ss 3737  df-pr 4319  df-tp 4321
This theorem is referenced by:  fr3nr  7124  rngplusg  16203  srngplusg  16211  lmodplusg  16220  ipsaddg  16227  ipsvsca  16230  phlplusg  16237  topgrpplusg  16245  otpstset  16254  otpstsetOLD  16258  odrngplusg  16269  odrngle  16272  prdsplusg  16319  prdsvsca  16321  prdsle  16323  imasplusg  16378  imasvsca  16381  imasle  16384  fuchom  16821  setchomfval  16929  catchomfval  16948  estrchomfval  16966  xpchomfval  17020  psrplusg  19589  psrvscafval  19598  cnfldadd  19959  cnfldle  19963  trkgdist  25559  algaddg  38268  clsk1indlem4  38861  rngchomfvalALTV  42505  ringchomfvalALTV  42568
  Copyright terms: Public domain W3C validator