Theorem elpw2g 4600

Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.)

Assertion

Ref	Expression
elpw2g	|- ( B e. V -> ( A e. ~P B <-> A C_ B ) )

Proof of Theorem elpw2g

Step	Hyp	Ref	Expression
1		elpwi 4008	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4583	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 4007	. . . . 5 |- ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4	3	biimparc 485	. . . 4 |- ( ( A C_ B /\ A e. _V ) -> A e. ~P B )
5	2, 4	syldan 468	. . 3 |- ( ( A C_ B /\ B e. V ) -> A e. ~P B )
6	5	expcom 433	. 2 |- ( B e. V -> ( A C_ B -> A e. ~P B ) )
7	1, 6	impbid2 204	1 |- ( B e. V -> ( A e. ~P B <-> A C_ B ) )

Syntax hints:   -> wi 4   <-> wb 184   e. wcel 1823   _Vcvv 3106   C_ wss 3461   ~Pcpw 3999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-ss 3475  df-pw 4001

This theorem is referenced by:  elpw2  4601  pwnss  4602  knatar  6228  pw2f1olem  7614  fineqvlem  7727  elfir  7867  marypha1  7886  r1sscl  8194  tskwe  8322  dfac8alem  8401  acni2  8418  fin1ai  8664  fin2i  8666  fin23lem7  8687  fin23lem11  8688  isfin2-2  8690  fin23lem39  8721  isf34lem1  8743  isf34lem2  8744  isf34lem4  8748  isf34lem5  8749  fin1a2lem7  8777  fin1a2lem12  8782  canthnumlem  9015  canthp1lem2  9020  wunss  9079  tsken  9121  tskss  9125  gruss  9163  ramub1lem1  14628  ismre  15079  mreintcl  15084  mremre  15093  submre  15094  mrcval  15099  mrccl  15100  mrcun  15111  ismri  15120  mreexd  15131  mreexexlem4d  15136  acsfiel  15143  isacs1i  15146  catcoppccl  15586  acsdrsel  15996  acsdrscl  15999  acsficl  16000  pmtrval  16675  pmtrrn  16681  opsrval  18334  istopg  19571  uniopn  19573  iscld  19695  ntrval  19704  clsval  19705  discld  19757  mretopd  19760  neival  19770  isnei  19771  lpval  19807  restdis  19846  ordtbaslem  19856  ordtuni  19858  cncls  19942  cndis  19959  tgcmp  20068  hauscmplem  20073  comppfsc  20199  elkgen  20203  xkoopn  20256  elqtop  20364  kqffn  20392  isfbas  20496  filss  20520  snfbas  20533  elfg  20538  fbasrn  20551  ufilss  20572  fixufil  20589  cfinufil  20595  ufinffr  20596  ufilen  20597  fin1aufil  20599  rnelfmlem  20619  flimclslem  20651  hauspwpwf1  20654  supnfcls  20687  flimfnfcls  20695  ptcmplem1  20718  tsmsfbas  20792  blfvalps  21052  blfps  21075  blf  21076  bcthlem5  21933  minveclem3b  22009  sigaclcuni  28348  sigaclcu2  28350  pwsiga  28360  erdsze2lem2  28912  cvmsval  28975  cvmsss2  28983  fin2so  30280  neibastop2lem  30418  tailf  30433  sdclem1  30476  elrfirn  30867  elrfirn2  30868  istopclsd  30872  nacsfix  30884  dnnumch1  31229