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

Theorem elpwg 3537
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 4063. (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 2313 . 2  |-  ( x  =  A  ->  (
x  e.  ~P B  <->  A  e.  ~P B ) )
2 sseq1 3120 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 vex 2730 . . 3  |-  x  e. 
_V
43elpw 3536 . 2  |-  ( x  e.  ~P B  <->  x  C_  B
)
51, 2, 4vtoclbg 2782 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 1621    C_ wss 3078   ~Pcpw 3530
This theorem is referenced by:  elpwi  3538  pwidg  3541  elpw2g  4063  pwel  4119  eldifpw  4457  elpwun  4458  elpwunsn  4459  f1opw2  5923  elpmg  6672  fopwdom  6855  elfpw  7041  f1opwfi  7043  rankwflemb  7349  r1elwf  7352  r1pw  7401  ackbij1lem3  7732  ackbij1lem6  7735  ackbij1lem11  7740  acsfn  13405  fiinopn  16479  clsval2  16619  ssntr  16627  nrmsep3  16915  cnrmi  16920  cmpcov  16948  cmpsublem  16958  concompss  16991  kgeni  17064  tgqtop  17235  filss  17380  ufileu  17446  filufint  17447  issubgo  20800  limsucncmpi  24058  inpws1  24207  caytr  24566  ismrcd1  25939  stoweidlem50  26933  stoweidlem57  26940  elpwgded  27120  snelpwrVD  27393  elpwgdedVD  27480  sspwimpcf  27483  sspwimpcfVD  27484  sspwimpALT2  27492
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089  df-pw 3532
  Copyright terms: Public domain W3C validator