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

Theorem snsstp2 4501
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 4499 . . 3 {𝐵} ⊆ {𝐴, 𝐵}
2 ssun1 3937 . . 3 {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
31, 2sstri 3769 . 2 {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4 df-tp 4338 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
53, 4sseqtr4i 3797 1 {𝐵} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3729  wss 3731  {csn 4333  {cpr 4335  {ctp 4337
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-v 3351  df-un 3736  df-in 3738  df-ss 3745  df-pr 4336  df-tp 4338
This theorem is referenced by:  fr3nr  7176  rngplusg  16275  srngplusg  16283  lmodplusg  16292  ipsaddg  16299  ipsvsca  16302  phlplusg  16309  topgrpplusg  16317  otpstset  16324  odrngplusg  16335  odrngle  16338  prdsplusg  16385  prdsvsca  16387  prdsle  16389  imasplusg  16444  imasvsca  16447  imasle  16450  fuchom  16887  setchomfval  16995  catchomfval  17014  estrchomfval  17032  xpchomfval  17086  psrplusg  19654  psrvscafval  19663  cnfldadd  20023  cnfldle  20027  trkgdist  25635  algaddg  38358  clsk1indlem4  38948  rngchomfvalALTV  42585  ringchomfvalALTV  42648
  Copyright terms: Public domain W3C validator