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

Theorem snelpwi 4299
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 3838 . 2  |-  ( A  e.  B  ->  { A }  C_  B )
2 snex 4295 . . 3  |-  { A }  e.  _V
32elpw 3707 . 2  |-  ( { A }  e.  ~P B 
<->  { A }  C_  B )
41, 3sylibr 203 1  |-  ( A  e.  B  ->  { A }  e.  ~P B
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710    C_ wss 3228   ~Pcpw 3701   {csn 3716
This theorem is referenced by:  unipw  4303  canth2  7099  unifpw  7245  marypha1lem  7273  infpwfidom  7742  ackbij1lem4  7936  acsfn  13654  sylow2a  15023  txdis  17426  txdis1cn  17429  symgtgp  17880  esumcst  23721  cntnevol  23846  coinflippvt  23991  onsucsuccmpi  25441  locfindis  25629  lpirlnr  26644  snelpwrOLD  28352  unipwrVD  28353  unipwr  28354  pclfinN  30141
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pr 4293
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-pw 3703  df-sn 3722  df-pr 3723
  Copyright terms: Public domain W3C validator