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

Theorem snelpwi 4607
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 4088 . 2  |-  ( A  e.  B  ->  { A }  C_  B )
2 snex 4603 . . 3  |-  { A }  e.  _V
32elpw 3933 . 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 1826    C_ wss 3389   ~Pcpw 3927   {csn 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-pw 3929  df-sn 3945  df-pr 3947
This theorem is referenced by:  unipw  4612  canth2  7589  unifpw  7738  marypha1lem  7808  infpwfidom  8322  ackbij1lem4  8516  acsfn  15066  sylow2a  16756  dissnref  20114  dissnlocfin  20115  locfindis  20116  txdis  20218  txdis1cn  20221  symgtgp  20685  dispcmp  28016  esumcst  28211  cntnevol  28355  coinflippvt  28606  onsucsuccmpi  30061  lpirlnr  31234  lincvalsng  33217  snlindsntor  33272  unipwrVD  33978  unipwr  33979  pclfinN  36037
  Copyright terms: Public domain W3C validator