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

Theorem snsstp1 4171
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 4169 . . 3  |-  { A }  C_  { A ,  B }
2 ssun1 3660 . . 3  |-  { A ,  B }  C_  ( { A ,  B }  u.  { C } )
31, 2sstri 3506 . 2  |-  { A }  C_  ( { A ,  B }  u.  { C } )
4 df-tp 4025 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
53, 4sseqtr4i 3530 1  |-  { A }  C_  { A ,  B ,  C }
Colors of variables: wff setvar class
Syntax hints:    u. cun 3467    C_ wss 3469   {csn 4020   {cpr 4022   {ctp 4024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-un 3474  df-in 3476  df-ss 3483  df-pr 4023  df-tp 4025
This theorem is referenced by:  fr3nr  6586  rngbase  14592  srngbase  14600  lmodbase  14609  ipsbase  14616  ipssca  14619  phlbase  14626  topgrpbas  14634  otpsbas  14641  odrngbas  14652  odrngtset  14655  prdssca  14700  prdsbas  14701  prdstset  14710  imasbas  14756  imassca  14763  imastset  14766  fucbas  15176  setcbas  15252  catcbas  15271  xpcbas  15294  psrbas  17794  psrbasOLD  17795  psrsca  17806  cnfldbas  18188  cnfldtset  18192  trkgbas  23562  signswch  28008  algbase  30585
  Copyright terms: Public domain W3C validator