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

Theorem snssg 3767
Description: The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.)
Assertion
Ref Expression
snssg  |-  ( A  e.  V  ->  ( A  e.  B  <->  { A }  C_  B ) )

Proof of Theorem snssg
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eleq1 2356 . 2  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
2 sneq 3664 . . 3  |-  ( x  =  A  ->  { x }  =  { A } )
32sseq1d 3218 . 2  |-  ( x  =  A  ->  ( { x }  C_  B 
<->  { A }  C_  B ) )
4 vex 2804 . . 3  |-  x  e. 
_V
54snss 3761 . 2  |-  ( x  e.  B  <->  { x }  C_  B )
61, 3, 5vtoclbg 2857 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  { A }  C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    e. wcel 1696    C_ wss 3165   {csn 3653
This theorem is referenced by:  snssi  3775  snssd  3776  prssg  3786  fr3nr  4587  fvimacnvALT  5660  vdwapid1  13038  acsfn  13577  cycsubg2  14670  cycsubg2cl  14671  pgpfac1lem1  15325  pgpfac1lem3a  15327  pgpfac1lem3  15328  pgpfac1lem5  15330  pgpfaclem2  15333  lspsnid  15766  lidldvgen  16023  frgpcyg  16543  isneip  16858  elnei  16864  cnpnei  17009  nlly2i  17218  1stckgenlem  17264  flimopn  17686  flimclslem  17695  fclsneii  17728  fcfnei  17746  limcvallem  19237  ellimc2  19243  limcflf  19247  limccnp  19257  limccnp2  19258  limcco  19259  lhop2  19378  plyrem  19701  isppw  20368  h1did  22146  ballotlemfp1  23066  erdszelem8  23744  cnfilca  25659  iscnp4  25666  neibastop2  26413  prnc  26795  proot1mul  27618
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-sn 3659
  Copyright terms: Public domain W3C validator