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

Theorem elpw2g 4168
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
StepHypRef Expression
1 elpwi 3634 . 2  |-  ( A  e.  ~P B  ->  A  C_  B )
2 ssexg 4161 . . . 4  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
3 elpwg 3633 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
43biimparc 475 . . . 4  |-  ( ( A  C_  B  /\  A  e.  _V )  ->  A  e.  ~P B
)
52, 4syldan 458 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  ~P B
)
65expcom 426 . 2  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  e.  ~P B ) )
71, 6impbid2 197 1  |-  ( B  e.  V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    e. wcel 1688   _Vcvv 2789    C_ wss 3153   ~Pcpw 3626
This theorem is referenced by:  elpw2  4169  knatar  5818  pwnss  6292  pw2f1olem  6961  fineqvlem  7072  elfir  7164  marypha1  7182  r1sscl  7452  tskwe  7578  dfac8alem  7651  acni2  7668  fin1ai  7914  fin2i  7916  fin23lem7  7937  fin23lem11  7938  isfin2-2  7940  fin23lem39  7971  isf34lem1  7993  isf34lem2  7994  isf34lem4  7998  isf34lem5  7999  fin1a2lem7  8027  fin1a2lem12  8032  canthnumlem  8265  canthp1lem2  8270  wunss  8329  tsken  8371  tskss  8375  gruss  8413  ramub1lem1  13067  ismre  13486  mreintcl  13491  mremre  13500  submre  13501  mrcval  13506  mrccl  13507  mrcun  13518  ismri  13527  mreexd  13538  mreexexlem4d  13543  acsfiel  13550  isacs1i  13553  catcoppccl  13934  acsdrsel  14264  acsdrscl  14267  acsficl  14268  opsrval  16210  istopg  16635  uniopn  16637  iscld  16758  ntrval  16767  clsval  16768  discld  16820  mretopd  16823  neiss2  16832  neival  16833  isnei  16834  lpval  16865  restdis  16903  ordtbaslem  16912  ordtuni  16914  cncls  16997  cndis  17013  tgcmp  17122  hauscmplem  17127  elkgen  17225  xkoopn  17278  elqtop  17382  kqffn  17410  isfbas  17518  filss  17542  snfbas  17555  elfg  17560  fbasrn  17573  ufilss  17594  fixufil  17611  cfinufil  17617  ufinffr  17618  ufilen  17619  fin1aufil  17621  rnelfmlem  17641  flimclslem  17673  hauspwpwf1  17676  supnfcls  17709  flimfnfcls  17717  ptcmplem1  17740  tsmsfbas  17804  blfval  17941  blf  17955  bcthlem5  18744  minveclem3b  18786  erdsze2lem2  23139  cvmsval  23201  cvmsss2  23209  ump  24444  islimrs  24979  comppfsc  25706  neibastop2lem  25708  tailf  25723  sdclem1  25852  elrfirn  26169  elrfirn2  26170  istopclsd  26174  nacsfix  26186  dnnumch1  26540  pmtrval  26793  pmtrrn  26798
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265  ax-sep 4142
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-pw 3628
  Copyright terms: Public domain W3C validator