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

Theorem snssg 4012
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 2503 . 2  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
2 sneq 3892 . . 3  |-  ( x  =  A  ->  { x }  =  { A } )
32sseq1d 3388 . 2  |-  ( x  =  A  ->  ( { x }  C_  B 
<->  { A }  C_  B ) )
4 vex 2980 . . 3  |-  x  e. 
_V
54snss 4004 . 2  |-  ( x  e.  B  <->  { x }  C_  B )
61, 3, 5vtoclbg 3036 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  { A }  C_  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369    e. wcel 1756    C_ wss 3333   {csn 3882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-v 2979  df-in 3340  df-ss 3347  df-sn 3883
This theorem is referenced by:  tppreqb  4019  snssi  4022  snssd  4023  prssg  4033  fvimacnvALT  5827  fr3nr  6396  vdwapid1  14041  acsfn  14602  cycsubg2  15723  cycsubg2cl  15724  pgpfac1lem1  16580  pgpfac1lem3a  16582  pgpfac1lem3  16583  pgpfac1lem5  16585  pgpfaclem2  16588  lspsnid  17079  lidldvgen  17342  isneip  18714  elnei  18720  iscnp4  18872  cnpnei  18873  nlly2i  19085  1stckgenlem  19131  flimopn  19553  flimclslem  19562  fclsneii  19595  fcfnei  19613  limcvallem  21351  ellimc2  21357  limcflf  21361  limccnp  21371  limccnp2  21372  limcco  21373  lhop2  21492  plyrem  21776  isppw  22457  h1did  24959  erdszelem8  27091  neibastop2  28587  prnc  28872  proot1mul  29569
  Copyright terms: Public domain W3C validator