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

Theorem elpw2g 4190
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 3646 . 2  |-  ( A  e.  ~P B  ->  A  C_  B )
2 ssexg 4176 . . . 4  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  _V )
3 elpwg 3645 . . . . 5  |-  ( A  e.  _V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
43biimparc 473 . . . 4  |-  ( ( A  C_  B  /\  A  e.  _V )  ->  A  e.  ~P B
)
52, 4syldan 456 . . 3  |-  ( ( A  C_  B  /\  B  e.  V )  ->  A  e.  ~P B
)
65expcom 424 . 2  |-  ( B  e.  V  ->  ( A  C_  B  ->  A  e.  ~P B ) )
71, 6impbid2 195 1  |-  ( B  e.  V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    e. wcel 1696   _Vcvv 2801    C_ wss 3165   ~Pcpw 3638
This theorem is referenced by:  elpw2  4191  pwnss  4192  knatar  5873  pw2f1olem  6982  fineqvlem  7093  elfir  7185  marypha1  7203  r1sscl  7473  tskwe  7599  dfac8alem  7672  acni2  7689  fin1ai  7935  fin2i  7937  fin23lem7  7958  fin23lem11  7959  isfin2-2  7961  fin23lem39  7992  isf34lem1  8014  isf34lem2  8015  isf34lem4  8019  isf34lem5  8020  fin1a2lem7  8048  fin1a2lem12  8053  canthnumlem  8286  canthp1lem2  8291  wunss  8350  tsken  8392  tskss  8396  gruss  8434  ramub1lem1  13089  ismre  13508  mreintcl  13513  mremre  13522  submre  13523  mrcval  13528  mrccl  13529  mrcun  13540  ismri  13549  mreexd  13560  mreexexlem4d  13565  acsfiel  13572  isacs1i  13575  catcoppccl  13956  acsdrsel  14286  acsdrscl  14289  acsficl  14290  opsrval  16232  istopg  16657  uniopn  16659  iscld  16780  ntrval  16789  clsval  16790  discld  16842  mretopd  16845  neiss2  16854  neival  16855  isnei  16856  lpval  16887  restdis  16925  ordtbaslem  16934  ordtuni  16936  cncls  17019  cndis  17035  tgcmp  17144  hauscmplem  17149  elkgen  17247  xkoopn  17300  elqtop  17404  kqffn  17432  isfbas  17540  filss  17564  snfbas  17577  elfg  17582  fbasrn  17595  ufilss  17616  fixufil  17633  cfinufil  17639  ufinffr  17640  ufilen  17641  fin1aufil  17643  rnelfmlem  17663  flimclslem  17695  hauspwpwf1  17698  supnfcls  17731  flimfnfcls  17739  ptcmplem1  17762  tsmsfbas  17826  blfval  17963  blf  17977  bcthlem5  18766  minveclem3b  18808  sigaclcuni  23494  sigaclcu2  23496  erdsze2lem2  23750  cvmsval  23812  cvmsss2  23820  ump  25149  islimrs  25683  comppfsc  26410  neibastop2lem  26412  tailf  26427  sdclem1  26556  elrfirn  26873  elrfirn2  26874  istopclsd  26878  nacsfix  26890  dnnumch1  27244  pmtrval  27497  pmtrrn  27502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-pw 3640
  Copyright terms: Public domain W3C validator