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

Theorem snsstp1 4167
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 4165 . . 3  |-  { A }  C_  { A ,  B }
2 ssun1 3653 . . 3  |-  { A ,  B }  C_  ( { A ,  B }  u.  { C } )
31, 2sstri 3498 . 2  |-  { A }  C_  ( { A ,  B }  u.  { C } )
4 df-tp 4021 . 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 4016   {cpr 4018   {ctp 4020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-in 3468  df-ss 3475  df-pr 4019  df-tp 4021
This theorem is referenced by:  fr3nr  6588  rngbase  14836  srngbase  14844  lmodbase  14853  ipsbase  14860  ipssca  14863  phlbase  14870  topgrpbas  14878  otpsbas  14885  odrngbas  14896  odrngtset  14899  prdssca  14945  prdsbas  14946  prdstset  14955  imasbas  15001  imassca  15008  imastset  15011  fucbas  15448  setcbas  15556  catcbas  15575  estrcbas  15593  xpcbas  15646  psrbas  18225  psrbasOLD  18226  psrsca  18237  cnfldbas  18619  cnfldtset  18623  trkgbas  24039  signswch  28782  algbase  31368  rngcbasALTV  33045  ringcbasALTV  33108
  Copyright terms: Public domain W3C validator