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

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

Proof of Theorem elpwg
StepHypRef Expression
1 eleq1 2344 . 2  |-  ( x  =  A  ->  (
x  e.  ~P B  <->  A  e.  ~P B ) )
2 sseq1 3200 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 vex 2792 . . 3  |-  x  e. 
_V
43elpw 3632 . 2  |-  ( x  e.  ~P B  <->  x  C_  B
)
51, 2, 4vtoclbg 2845 1  |-  ( A  e.  V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    e. wcel 1688    C_ wss 3153   ~Pcpw 3626
This theorem is referenced by:  elpwi  3634  pwidg  3638  elpw2g  4168  pwel  4224  eldifpw  4565  elpwun  4566  elpwunsn  4567  f1opw2  6032  elpmg  6781  fopwdom  6965  elfpw  7152  f1opwfi  7154  rankwflemb  7460  r1elwf  7463  r1pw  7512  ackbij1lem3  7843  ackbij1lem6  7846  ackbij1lem11  7851  mreexexlemd  13540  acsfn  13555  fiinopn  16641  clsval2  16781  ssntr  16789  nrmsep3  17077  cnrmi  17082  cmpcov  17110  cmpsublem  17120  concompss  17153  kgeni  17226  tgqtop  17397  filss  17542  ufileu  17608  filufint  17609  issubgo  20962  ballotlemelo  23039  ballotlemfmpn  23046  limsucncmpi  24291  inpws1  24440  caytr  24799  ismrcd1  26172  stoweidlem50  27198  stoweidlem57  27205  elpwgded  27601  snelpwrVD  27874  elpwgdedVD  27961  sspwimpcf  27964  sspwimpcfVD  27965  sspwimpALT2  27973
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-pw 3628
  Copyright terms: Public domain W3C validator