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

Theorem elpwg 3798
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 4355. (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 2495 . 2  |-  ( x  =  A  ->  (
x  e.  ~P B  <->  A  e.  ~P B ) )
2 sseq1 3361 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 vex 2951 . . 3  |-  x  e. 
_V
43elpw 3797 . 2  |-  ( x  e.  ~P B  <->  x  C_  B
)
51, 2, 4vtoclbg 3004 1  |-  ( A  e.  V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    e. wcel 1725    C_ wss 3312   ~Pcpw 3791
This theorem is referenced by:  elpwi  3799  pwidg  3803  prsspwg  3947  prsspwgOLD  3948  elpw2g  4355  pwel  4407  eldifpw  4746  elpwun  4747  elpwunsn  4748  f1opw2  6289  elpmg  7023  fopwdom  7207  elfpw  7399  f1opwfi  7401  rankwflemb  7708  r1elwf  7711  r1pw  7760  ackbij1lem3  8091  ackbij1lem6  8094  ackbij1lem11  8099  mreexexlemd  13857  acsfn  13872  fiinopn  16962  clsval2  17102  ssntr  17110  neipeltop  17181  nrmsep3  17407  cnrmi  17412  cmpcov  17440  cmpsublem  17450  concompss  17484  kgeni  17557  tgqtop  17732  filss  17873  ufileu  17939  filufint  17940  ustssel  18223  elutop  18251  ustuqtop0  18258  metustssOLD  18571  metustss  18572  metutopOLD  18600  psmetutop  18601  issubgo  21879  indval  24399  isrnsigaOLD  24483  sigaclci  24503  sigainb  24507  elsigagen2  24519  measvunilem  24554  measdivcstOLD  24566  limsucncmpi  26143  ismrcd1  26689  stoweidlem50  27713  stoweidlem57  27720  elpwgded  28506  snelpwrVD  28797  elpwgdedVD  28883  sspwimpcf  28886  sspwimpcfVD  28887  sspwimpALT2  28895
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-ss 3326  df-pw 3793
  Copyright terms: Public domain W3C validator