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

Theorem snsstp1 4122
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 4120 . . 3  |-  { A }  C_  { A ,  B }
2 ssun1 3617 . . 3  |-  { A ,  B }  C_  ( { A ,  B }  u.  { C } )
31, 2sstri 3463 . 2  |-  { A }  C_  ( { A ,  B }  u.  { C } )
4 df-tp 3980 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
53, 4sseqtr4i 3487 1  |-  { A }  C_  { A ,  B ,  C }
Colors of variables: wff setvar class
Syntax hints:    u. cun 3424    C_ wss 3426   {csn 3975   {cpr 3977   {ctp 3979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3070  df-un 3431  df-in 3433  df-ss 3440  df-pr 3978  df-tp 3980
This theorem is referenced by:  fr3nr  6491  rngbase  14388  srngbase  14396  lmodbase  14405  ipsbase  14412  ipssca  14415  phlbase  14422  topgrpbas  14430  otpsbas  14437  odrngbas  14448  odrngtset  14451  prdssca  14496  prdsbas  14497  prdstset  14506  imasbas  14552  imassca  14559  imastset  14562  fucbas  14972  setcbas  15048  catcbas  15067  xpcbas  15090  psrbas  17554  psrbasOLD  17555  psrsca  17566  cnfldbas  17931  cnfldtset  17935  trkgbas  23021  signswch  27096  algbase  29673
  Copyright terms: Public domain W3C validator