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

Theorem elpw2g 4107
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 3574 . 2  |-  ( A  e.  ~P B  ->  A  C_  B )
2 ssexg 4100 . . . 4  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
3 elpwg 3573 . . . . 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 1621   _Vcvv 2740    C_ wss 3094   ~Pcpw 3566
This theorem is referenced by:  elpw2  4108  knatar  5756  pwnss  6230  pw2f1olem  6899  fineqvlem  7010  elfir  7102  marypha1  7120  r1sscl  7390  tskwe  7516  dfac8alem  7589  acni2  7606  fin1ai  7852  fin2i  7854  fin23lem7  7875  fin23lem11  7876  isfin2-2  7878  fin23lem39  7909  isf34lem1  7931  isf34lem2  7932  isf34lem4  7936  isf34lem5  7937  fin1a2lem7  7965  fin1a2lem12  7970  canthnumlem  8203  canthp1lem2  8208  wunss  8267  tsken  8309  tskss  8313  gruss  8351  ramub1lem1  13000  ismre  13419  mreintcl  13424  mremre  13433  submre  13434  mrcval  13439  mrccl  13440  mrcun  13451  ismri  13460  mreexd  13471  mreexexlem4d  13476  acsfiel  13483  isacs1i  13486  catcoppccl  13867  acsdrsel  14197  acsdrscl  14200  acsficl  14201  opsrval  16143  istopg  16568  uniopn  16570  iscld  16691  ntrval  16700  clsval  16701  discld  16753  mretopd  16756  neiss2  16765  neival  16766  isnei  16767  lpval  16798  restdis  16836  ordtbaslem  16845  ordtuni  16847  cncls  16930  cndis  16946  tgcmp  17055  hauscmplem  17060  elkgen  17158  xkoopn  17211  elqtop  17315  kqffn  17343  isfbas  17451  filss  17475  snfbas  17488  elfg  17493  fbasrn  17506  ufilss  17527  fixufil  17544  cfinufil  17550  ufinffr  17551  ufilen  17552  fin1aufil  17554  rnelfmlem  17574  flimclslem  17606  hauspwpwf1  17609  supnfcls  17642  flimfnfcls  17650  ptcmplem1  17673  tsmsfbas  17737  blfval  17874  blf  17888  bcthlem5  18677  minveclem3b  18719  erdsze2lem2  23072  cvmsval  23134  cvmsss2  23142  ump  24377  islimrs  24912  comppfsc  25639  neibastop2lem  25641  tailf  25656  sdclem1  25785  elrfirn  26102  elrfirn2  26103  istopclsd  26107  nacsfix  26119  dnnumch1  26473  pmtrval  26726  pmtrrn  26731
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 2237  ax-sep 4081
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108  df-pw 3568
  Copyright terms: Public domain W3C validator