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

Theorem snsspr1 3764
Description: A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)
Assertion
Ref Expression
snsspr1  |-  { A }  C_  { A ,  B }

Proof of Theorem snsspr1
StepHypRef Expression
1 ssun1 3338 . 2  |-  { A }  C_  ( { A }  u.  { B } )
2 df-pr 3647 . 2  |-  { A ,  B }  =  ( { A }  u.  { B } )
31, 2sseqtr4i 3211 1  |-  { A }  C_  { A ,  B }
Colors of variables: wff set class
Syntax hints:    u. cun 3150    C_ wss 3152   {csn 3640   {cpr 3641
This theorem is referenced by:  snsstp1  3766  uniop  4269  op1stb  4569  rankopb  7524  ltrelxr  8886  2strbas  13245  algsca  13281  phlvsca  13291  prdssca  13356  prdshom  13366  imassca  13422  ipobas  14258  ipolerval  14259  lspprid1  15754  lsppratlem3  15902  lsppratlem4  15903  ex-dif  20810  ex-un  20811  ex-in  20812  coinflippv  23684  subfacp1lem2a  23711  altopthsn  24495  rankaltopb  24513  dvh3dim3N  31639  mapdindp2  31911  lspindp5  31960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-pr 3647
  Copyright terms: Public domain W3C validator