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

Theorem snsstp1 4166
Description: A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
Assertion
Ref Expression
snsstp1  |-  { A }  C_  { A ,  B ,  C }

Proof of Theorem snsstp1
StepHypRef Expression
1 snsspr1 4164 . . 3  |-  { A }  C_  { A ,  B }
2 ssun1 3652 . . 3  |-  { A ,  B }  C_  ( { A ,  B }  u.  { C } )
31, 2sstri 3498 . 2  |-  { A }  C_  ( { A ,  B }  u.  { C } )
4 df-tp 4019 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
53, 4sseqtr4i 3522 1  |-  { A }  C_  { A ,  B ,  C }
Colors of variables: wff setvar class
Syntax hints:    u. cun 3459    C_ wss 3461   {csn 4014   {cpr 4016   {ctp 4018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-in 3468  df-ss 3475  df-pr 4017  df-tp 4019
This theorem is referenced by:  fr3nr  6600  rngbase  14622  srngbase  14630  lmodbase  14639  ipsbase  14646  ipssca  14649  phlbase  14656  topgrpbas  14664  otpsbas  14671  odrngbas  14682  odrngtset  14685  prdssca  14730  prdsbas  14731  prdstset  14740  imasbas  14786  imassca  14793  imastset  14796  fucbas  15203  setcbas  15279  catcbas  15298  xpcbas  15321  psrbas  17904  psrbasOLD  17905  psrsca  17916  cnfldbas  18298  cnfldtset  18302  trkgbas  23713  signswch  28391  algbase  31103  estrcbas  32480  rngcbasOLD  32531  ringcbasOLD  32591
  Copyright terms: Public domain W3C validator