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

Theorem elpwg 3606
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 4141. (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 2318 . 2  |-  ( x  =  A  ->  (
x  e.  ~P B  <->  A  e.  ~P B ) )
2 sseq1 3174 . 2  |-  ( x  =  A  ->  (
x  C_  B  <->  A  C_  B
) )
3 vex 2766 . . 3  |-  x  e. 
_V
43elpw 3605 . 2  |-  ( x  e.  ~P B  <->  x  C_  B
)
51, 2, 4vtoclbg 2819 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 3127   ~Pcpw 3599
This theorem is referenced by:  elpwi  3607  pwidg  3611  elpw2g  4141  pwel  4197  eldifpw  4538  elpwun  4539  elpwunsn  4540  f1opw2  6005  elpmg  6754  fopwdom  6938  elfpw  7125  f1opwfi  7127  rankwflemb  7433  r1elwf  7436  r1pw  7485  ackbij1lem3  7816  ackbij1lem6  7819  ackbij1lem11  7824  mreexexlemd  13508  acsfn  13523  fiinopn  16609  clsval2  16749  ssntr  16757  nrmsep3  17045  cnrmi  17050  cmpcov  17078  cmpsublem  17088  concompss  17121  kgeni  17194  tgqtop  17365  filss  17510  ufileu  17576  filufint  17577  issubgo  20930  ballotlemelo  23007  ballotlemfmpn  23014  limsucncmpi  24259  inpws1  24408  caytr  24767  ismrcd1  26140  stoweidlem50  27134  stoweidlem57  27141  elpwgded  27383  snelpwrVD  27656  elpwgdedVD  27743  sspwimpcf  27746  sspwimpcfVD  27747  sspwimpALT2  27755
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 1927  ax-ext 2239
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141  df-pw 3601
  Copyright terms: Public domain W3C validator