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

Theorem elpwg 3632
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 4174. (Contributed by NM, 6-Aug-2000.)
Assertion
Ref Expression
elpwg  |-  ( A  e.  V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )

Proof of Theorem elpwg
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eleq1 2343 . 2  |-  ( x  =  A  ->  (
x  e.  ~P B  <->  A  e.  ~P B ) )
2 sseq1 3199 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 vex 2791 . . 3  |-  x  e. 
_V
43elpw 3631 . 2  |-  ( x  e.  ~P B  <->  x  C_  B
)
51, 2, 4vtoclbg 2844 1  |-  ( A  e.  V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    e. wcel 1684    C_ wss 3152   ~Pcpw 3625
This theorem is referenced by:  elpwi  3633  pwidg  3637  elpw2g  4174  pwel  4225  eldifpw  4566  elpwun  4567  elpwunsn  4568  f1opw2  6071  elpmg  6786  fopwdom  6970  elfpw  7157  f1opwfi  7159  rankwflemb  7465  r1elwf  7468  r1pw  7517  ackbij1lem3  7848  ackbij1lem6  7851  ackbij1lem11  7856  mreexexlemd  13546  acsfn  13561  fiinopn  16647  clsval2  16787  ssntr  16795  nrmsep3  17083  cnrmi  17088  cmpcov  17116  cmpsublem  17126  concompss  17159  kgeni  17232  tgqtop  17403  filss  17548  ufileu  17614  filufint  17615  issubgo  20970  ballotlemelo  23046  ballotlemfmpn  23053  prsspwg  23184  prelpwi  23185  ishashinf  23389  sigaex  23470  sigaval  23471  isrnsigaOLD  23473  pwsiga  23491  sigaclci  23493  difelsiga  23494  unelsiga  23495  sigainb  23497  insiga  23498  sigagensiga  23502  elsigagen2  23509  measvunilem  23540  measdivcstOLD  23551  measdivcst  23552  indval  23597  probun  23622  coinfliprv  23683  limsucncmpi  24884  inpws1  25042  caytr  25400  ismrcd1  26773  stoweidlem50  27799  stoweidlem57  27806  prelpw  28074  elpwgded  28330  snelpwrVD  28606  elpwgdedVD  28693  sspwimpcf  28696  sspwimpcfVD  28697  sspwimpALT2  28705
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627
  Copyright terms: Public domain W3C validator