Theorem elpwg 3858

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. See also elpw2g 4445. (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.

Step	Hyp	Ref	Expression
1		eleq1 2495	. 2 |- ( x = A -> ( x e. ~P B <-> A e. ~P B ) )
2		sseq1 3367	. 2 |- ( x = A -> ( x C_ B <-> A C_ B ) )
3		selpw 3857	. 2 |- ( x e. ~P B <-> x C_ B )
4	1, 2, 3	vtoclbg 3022	1 |- ( A e. V -> ( A e. ~P B <-> A C_ B ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1757   C_ wss 3318   ~Pcpw 3850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2966  df-in 3325  df-ss 3332  df-pw 3852

This theorem is referenced by:  elpwi  3859  pwidg  3863  elpwunsn  3907  prsspwg  4020  elpw2g  4445  pwel  4534  f1opw2  6304  eldifpw  6379  elpwun  6380  elpmg  7218  fopwdom  7409  elfpw  7603  f1opwfi  7605  rankwflemb  7990  r1elwf  7993  r1pw  8042  ackbij1lem3  8381  ackbij1lem6  8384  ackbij1lem11  8389  mreexexlemd  14567  acsfn  14582  fiinopn  18358  clsval2  18498  ssntr  18506  neipeltop  18577  nrmsep3  18803  cnrmi  18808  cmpcov  18836  cmpsublem  18846  concompss  18881  kgeni  18954  tgqtop  19129  filss  19270  ufileu  19336  filufint  19337  ustssel  19624  elutop  19652  ustuqtop0  19659  metustssOLD  19972  metustss  19973  metutopOLD  20001  psmetutop  20002  axtgcont1  22816  issubgo  23615  fpwrelmap  25860  indval  26326  isrnsigaOLD  26411  sigaclci  26431  sigainb  26435  elsigagen2  26447  measvunilem  26482  measdivcstOLD  26494  ddeval1  26506  ddeval0  26507  limsucncmpi  28141  ismrcd1  28881  stoweidlem50  29693  stoweidlem57  29700  gsumlsscl  30629  lincfsuppcl  30696  linccl  30697  lincdifsn  30707  lincellss  30709  ellcoellss  30718  lindslinindsimp1  30740  lindslinindimp2lem4  30744  lindslinindsimp2lem5  30745  lindslinindsimp2  30746  lincresunit3lem2  30763  lincresunit3  30764  elpwgded  31014  snelpwrVD  31309  elpwgdedVD  31395  sspwimpcf  31398  sspwimpcfVD  31399  sspwimpALT2  31406