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

Theorem snssg 3900
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 2472 . 2  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
2 sneq 3793 . . 3  |-  ( x  =  A  ->  { x }  =  { A } )
32sseq1d 3343 . 2  |-  ( x  =  A  ->  ( { x }  C_  B 
<->  { A }  C_  B ) )
4 vex 2927 . . 3  |-  x  e. 
_V
54snss 3894 . 2  |-  ( x  e.  B  <->  { x }  C_  B )
61, 3, 5vtoclbg 2980 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  { A }  C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1721    C_ wss 3288   {csn 3782
This theorem is referenced by:  tppreqb  3907  snssi  3910  snssd  3911  prssg  3921  fr3nr  4727  fvimacnvALT  5816  vdwapid1  13306  acsfn  13847  cycsubg2  14940  cycsubg2cl  14941  pgpfac1lem1  15595  pgpfac1lem3a  15597  pgpfac1lem3  15598  pgpfac1lem5  15600  pgpfaclem2  15603  lspsnid  16032  lidldvgen  16289  frgpcyg  16817  isneip  17132  elnei  17138  iscnp4  17289  cnpnei  17290  nlly2i  17500  1stckgenlem  17546  flimopn  17968  flimclslem  17977  fclsneii  18010  fcfnei  18028  limcvallem  19719  ellimc2  19725  limcflf  19729  limccnp  19739  limccnp2  19740  limcco  19741  lhop2  19860  plyrem  20183  isppw  20858  h1did  23014  erdszelem8  24845  neibastop2  26288  prnc  26575  proot1mul  27391
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-in 3295  df-ss 3302  df-sn 3788
  Copyright terms: Public domain W3C validator