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

Theorem snssg 3924
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 2495 . 2  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
2 sneq 3817 . . 3  |-  ( x  =  A  ->  { x }  =  { A } )
32sseq1d 3367 . 2  |-  ( x  =  A  ->  ( { x }  C_  B 
<->  { A }  C_  B ) )
4 vex 2951 . . 3  |-  x  e. 
_V
54snss 3918 . 2  |-  ( x  e.  B  <->  { x }  C_  B )
61, 3, 5vtoclbg 3004 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  { A }  C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725    C_ wss 3312   {csn 3806
This theorem is referenced by:  tppreqb  3931  snssi  3934  snssd  3935  prssg  3945  fr3nr  4751  fvimacnvALT  5840  vdwapid1  13331  acsfn  13872  cycsubg2  14965  cycsubg2cl  14966  pgpfac1lem1  15620  pgpfac1lem3a  15622  pgpfac1lem3  15623  pgpfac1lem5  15625  pgpfaclem2  15628  lspsnid  16057  lidldvgen  16314  frgpcyg  16842  isneip  17157  elnei  17163  iscnp4  17315  cnpnei  17316  nlly2i  17527  1stckgenlem  17573  flimopn  17995  flimclslem  18004  fclsneii  18037  fcfnei  18055  limcvallem  19746  ellimc2  19752  limcflf  19756  limccnp  19766  limccnp2  19767  limcco  19768  lhop2  19887  plyrem  20210  isppw  20885  h1did  23041  erdszelem8  24872  neibastop2  26327  prnc  26614  proot1mul  27430
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326  df-sn 3812
  Copyright terms: Public domain W3C validator