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

Theorem snssg 3755
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
StepHypRef Expression
1 eleq1 2344 . 2  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
2 sneq 3652 . . 3  |-  ( x  =  A  ->  { x }  =  { A } )
32sseq1d 3206 . 2  |-  ( x  =  A  ->  ( { x }  C_  B 
<->  { A }  C_  B ) )
4 vex 2792 . . 3  |-  x  e. 
_V
54snss 3749 . 2  |-  ( x  e.  B  <->  { x }  C_  B )
61, 3, 5vtoclbg 2845 1  |-  ( A  e.  V  ->  ( A  e.  B  <->  { A }  C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    = wceq 1628    e. wcel 1688    C_ wss 3153   {csn 3641
This theorem is referenced by:  snssi  3760  snssd  3761  prssg  3771  fr3nr  4570  fvimacnvALT  5605  vdwapid1  13016  acsfn  13555  cycsubg2  14648  cycsubg2cl  14649  pgpfac1lem1  15303  pgpfac1lem3a  15305  pgpfac1lem3  15306  pgpfac1lem5  15308  pgpfaclem2  15311  lspsnid  15744  lidldvgen  16001  frgpcyg  16521  isneip  16836  elnei  16842  cnpnei  16987  nlly2i  17196  1stckgenlem  17242  flimopn  17664  flimclslem  17673  fclsneii  17706  fcfnei  17724  limcvallem  19215  ellimc2  19221  limcflf  19225  limccnp  19235  limccnp2  19236  limcco  19237  lhop2  19356  plyrem  19679  isppw  20346  h1did  22122  ballotlemfp1  23043  erdszelem8  23133  cnfilca  24955  iscnp4  24962  neibastop2  25709  prnc  26091  proot1mul  26914
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-sn 3647
  Copyright terms: Public domain W3C validator