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

Theorem snssg 3932
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 2496 . 2  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
2 sneq 3825 . . 3  |-  ( x  =  A  ->  { x }  =  { A } )
32sseq1d 3375 . 2  |-  ( x  =  A  ->  ( { x }  C_  B 
<->  { A }  C_  B ) )
4 vex 2959 . . 3  |-  x  e. 
_V
54snss 3926 . 2  |-  ( x  e.  B  <->  { x }  C_  B )
61, 3, 5vtoclbg 3012 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 3320   {csn 3814
This theorem is referenced by:  tppreqb  3939  snssi  3942  snssd  3943  prssg  3953  fr3nr  4760  fvimacnvALT  5849  vdwapid1  13343  acsfn  13884  cycsubg2  14977  cycsubg2cl  14978  pgpfac1lem1  15632  pgpfac1lem3a  15634  pgpfac1lem3  15635  pgpfac1lem5  15637  pgpfaclem2  15640  lspsnid  16069  lidldvgen  16326  frgpcyg  16854  isneip  17169  elnei  17175  iscnp4  17327  cnpnei  17328  nlly2i  17539  1stckgenlem  17585  flimopn  18007  flimclslem  18016  fclsneii  18049  fcfnei  18067  limcvallem  19758  ellimc2  19764  limcflf  19768  limccnp  19778  limccnp2  19779  limcco  19780  lhop2  19899  plyrem  20222  isppw  20897  h1did  23053  erdszelem8  24884  neibastop2  26390  prnc  26677  proot1mul  27492
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327  df-ss 3334  df-sn 3820
  Copyright terms: Public domain W3C validator