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

Theorem snssg 3754
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 2343 . 2  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
2 sneq 3651 . . 3  |-  ( x  =  A  ->  { x }  =  { A } )
32sseq1d 3205 . 2  |-  ( x  =  A  ->  ( { x }  C_  B 
<->  { A }  C_  B ) )
4 vex 2791 . . 3  |-  x  e. 
_V
54snss 3748 . 2  |-  ( x  e.  B  <->  { x }  C_  B )
61, 3, 5vtoclbg 2844 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  { A }  C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    e. wcel 1684    C_ wss 3152   {csn 3640
This theorem is referenced by:  snssi  3759  snssd  3760  prssg  3770  fr3nr  4571  fvimacnvALT  5644  vdwapid1  13022  acsfn  13561  cycsubg2  14654  cycsubg2cl  14655  pgpfac1lem1  15309  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfac1lem5  15314  pgpfaclem2  15317  lspsnid  15750  lidldvgen  16007  frgpcyg  16527  isneip  16842  elnei  16848  cnpnei  16993  nlly2i  17202  1stckgenlem  17248  flimopn  17670  flimclslem  17679  fclsneii  17712  fcfnei  17730  limcvallem  19221  ellimc2  19227  limcflf  19231  limccnp  19241  limccnp2  19242  limcco  19243  lhop2  19362  plyrem  19685  isppw  20352  h1did  22130  ballotlemfp1  23050  erdszelem8  23729  cnfilca  25556  iscnp4  25563  neibastop2  26310  prnc  26692  proot1mul  27515
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-in 3159  df-ss 3166  df-sn 3646
  Copyright terms: Public domain W3C validator