Theorem elpw2g 4827

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 4168	. 2 |- ( A e. ~P B -> A C_ B )
2		ssexg 4804	. . . 4 |- ( ( A C_ B /\ B e. V ) -> A e. _V )
3		elpwg 4166	. . . . 5 |- ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
4	3	biimparc 504	. . . 4 |- ( ( A C_ B /\ A e. _V ) -> A e. ~P B )
5	2, 4	syldan 487	. . 3 |- ( ( A C_ B /\ B e. V ) -> A e. ~P B )
6	5	expcom 451	. 2 |- ( B e. V -> ( A C_ B -> A e. ~P B ) )
7	1, 6	impbid2 216	1 |- ( B e. V -> ( A e. ~P B <-> A C_ B ) )

Syntax hints:   -> wi 4   <-> wb 196   e. wcel 1990   _Vcvv 3200   C_ wss 3574   ~Pcpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160

This theorem is referenced by:  elpw2  4828  elpwi2  4829  pwnss  4830  pw2f1olem  8064  fineqvlem  8174  elfir  8321  marypha1  8340  r1sscl  8648  tskwe  8776  dfac8alem  8852  acni2  8869  fin1ai  9115  fin2i  9117  fin23lem7  9138  fin23lem11  9139  isfin2-2  9141  fin23lem39  9172  isf34lem1  9194  isf34lem2  9195  isf34lem4  9199  isf34lem5  9200  fin1a2lem12  9233  canthnumlem  9470  canthp1lem2  9475  tsken  9576  tskss  9580  gruss  9618  ramub1lem1  15730  ismre  16250  mreintcl  16255  mremre  16264  submre  16265  mrcval  16270  mrccl  16271  mrcun  16282  ismri  16291  mreexexlem4d  16307  acsfiel  16315  isacs1i  16318  catcoppccl  16758  acsdrsel  17167  acsdrscl  17170  acsficl  17171  pmtrval  17871  pmtrrn  17877  opsrval  19474  istopg  20700  uniopn  20702  iscld  20831  ntrval  20840  clsval  20841  discld  20893  mretopd  20896  neival  20906  isnei  20907  lpval  20943  restdis  20982  ordtbaslem  20992  ordtuni  20994  cncls  21078  cndis  21095  tgcmp  21204  hauscmplem  21209  comppfsc  21335  elkgen  21339  xkoopn  21392  elqtop  21500  kqffn  21528  isfbas  21633  filss  21657  snfbas  21670  elfg  21675  fbasrn  21688  ufilss  21709  fixufil  21726  cfinufil  21732  ufinffr  21733  ufilen  21734  fin1aufil  21736  rnelfmlem  21756  flimclslem  21788  hauspwpwf1  21791  supnfcls  21824  flimfnfcls  21832  ptcmplem1  21856  tsmsfbas  21931  blfvalps  22188  blfps  22211  blf  22212  bcthlem5  23125  minveclem3b  23199  sigaclcuni  30181  sigaclcu2  30183  pwsiga  30193  erdsze2lem2  31186  cvmsval  31248  cvmsss2  31256  neibastop2lem  32355  tailf  32370  bj-ismoored  33062  fin2so  33396  sdclem1  33539  elrfirn  37258  elrfirn2  37259  istopclsd  37263  nacsfix  37275  dnnumch1  37614