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

Theorem snelpwi 4698
Description: A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.)
Assertion
Ref Expression
snelpwi  |-  ( A  e.  B  ->  { A }  e.  ~P B
)

Proof of Theorem snelpwi
StepHypRef Expression
1 snssi 4177 . 2  |-  ( A  e.  B  ->  { A }  C_  B )
2 snex 4694 . . 3  |-  { A }  e.  _V
32elpw 4022 . 2  |-  ( { A }  e.  ~P B 
<->  { A }  C_  B )
41, 3sylibr 212 1  |-  ( A  e.  B  ->  { A }  e.  ~P B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767    C_ wss 3481   ~Pcpw 4016   {csn 4033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pr 4692
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-pw 4018  df-sn 4034  df-pr 4036
This theorem is referenced by:  unipw  4703  canth2  7682  unifpw  7835  marypha1lem  7905  infpwfidom  8421  ackbij1lem4  8615  acsfn  14930  sylow2a  16510  dissnref  19895  dissnlocfin  19896  locfindis  19897  txdis  19999  txdis1cn  20002  symgtgp  20466  dispcmp  27694  esumcst  27903  cntnevol  28031  coinflippvt  28255  onsucsuccmpi  29842  lpirlnr  31000  lincvalsng  32504  snlindsntor  32559  unipwrVD  33118  unipwr  33119  pclfinN  35102
  Copyright terms: Public domain W3C validator