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

Theorem elpwg 3645
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 4190. (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 2356 . 2  |-  ( x  =  A  ->  (
x  e.  ~P B  <->  A  e.  ~P B ) )
2 sseq1 3212 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 vex 2804 . . 3  |-  x  e. 
_V
43elpw 3644 . 2  |-  ( x  e.  ~P B  <->  x  C_  B
)
51, 2, 4vtoclbg 2857 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 1696    C_ wss 3165   ~Pcpw 3638
This theorem is referenced by:  elpwi  3646  pwidg  3650  elpw2g  4190  pwel  4241  eldifpw  4582  elpwun  4583  elpwunsn  4584  f1opw2  6087  elpmg  6802  fopwdom  6986  elfpw  7173  f1opwfi  7175  rankwflemb  7481  r1elwf  7484  r1pw  7533  ackbij1lem3  7864  ackbij1lem6  7867  ackbij1lem11  7872  mreexexlemd  13562  acsfn  13577  fiinopn  16663  clsval2  16803  ssntr  16811  nrmsep3  17099  cnrmi  17104  cmpcov  17132  cmpsublem  17142  concompss  17175  kgeni  17248  tgqtop  17419  filss  17564  ufileu  17630  filufint  17631  issubgo  20986  ballotlemelo  23062  ballotlemfmpn  23069  prsspwg  23200  prelpwi  23201  ishashinf  23404  sigaex  23485  sigaval  23486  isrnsigaOLD  23488  pwsiga  23506  sigaclci  23508  difelsiga  23509  unelsiga  23510  sigainb  23512  insiga  23513  sigagensiga  23517  elsigagen2  23524  measvunilem  23555  measdivcstOLD  23566  measdivcst  23567  indval  23612  probun  23637  coinfliprv  23698  limsucncmpi  24956  inpws1  25145  caytr  25503  ismrcd1  26876  stoweidlem50  27902  stoweidlem57  27909  prelpw  28184  elpwgded  28629  snelpwrVD  28922  elpwgdedVD  29009  sspwimpcf  29012  sspwimpcfVD  29013  sspwimpALT2  29021
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-pw 3640
  Copyright terms: Public domain W3C validator