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

Theorem snsstp1 4287
 Description: A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
Assertion
Ref Expression
snsstp1 {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Proof of Theorem snsstp1
StepHypRef Expression
1 snsspr1 4285 . . 3 {𝐴} ⊆ {𝐴, 𝐵}
2 ssun1 3738 . . 3 {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
31, 2sstri 3577 . 2 {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4 df-tp 4130 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
53, 4sseqtr4i 3601 1 {𝐴} ⊆ {𝐴, 𝐵, 𝐶}
 Colors of variables: wff setvar class Syntax hints:   ∪ cun 3538   ⊆ wss 3540  {csn 4125  {cpr 4127  {ctp 4129 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-pr 4128  df-tp 4130 This theorem is referenced by:  fr3nr  6871  rngbase  15824  srngbase  15832  lmodbase  15841  ipsbase  15848  ipssca  15851  phlbase  15858  topgrpbas  15866  otpsbas  15875  otpsbasOLD  15879  odrngbas  15890  odrngtset  15893  prdssca  15939  prdsbas  15940  prdstset  15949  imasbas  15995  imassca  16002  imastset  16005  fucbas  16443  setcbas  16551  catcbas  16570  estrcbas  16588  xpcbas  16641  psrbas  19199  psrsca  19210  cnfldbas  19571  cnfldtset  19575  trkgbas  25144  signswch  29964  algbase  36767  clsk1indlem4  37362  clsk1indlem1  37363  rngcbasALTV  41775  ringcbasALTV  41838
 Copyright terms: Public domain W3C validator