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

Theorem elpwi 3775
Description: Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.)
Assertion
Ref Expression
elpwi  |-  ( A  e.  ~P B  ->  A  C_  B )

Proof of Theorem elpwi
StepHypRef Expression
1 elpwg 3774 . 2  |-  ( A  e.  ~P B  -> 
( A  e.  ~P B 
<->  A  C_  B )
)
21ibi 233 1  |-  ( A  e.  ~P B  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721    C_ wss 3288   ~Pcpw 3767
This theorem is referenced by:  elpwid  3776  elelpwi  3777  elpw2g  4331  eldifpw  4722  elpwunsn  4724  iunpw  4726  f1opw2  6265  f1opwfi  7376  fi0  7391  fiin  7393  marypha1lem  7404  marypha1  7405  marypha2  7410  brwdom2  7505  brwdom3  7514  r1pwss  7674  rankpwi  7713  acndom  7896  acnnum  7897  dfac12r  7990  ackbij2lem1  8063  ackbij1lem6  8069  ackbij1b  8083  isfin2-2  8163  ssfin2  8164  enfin2i  8165  compsscnvlem  8214  compssiso  8218  fin11a  8227  enfin1ai  8228  fin12  8257  fin1a2s  8258  fin1a2  8259  hsmexlem2  8271  tskwe2  8612  inttsk  8613  inatsk  8617  hashbclem  11664  qshash  12569  incexclem  12579  incexc  12580  incexc2  12581  rpnnen2  12788  smupf  12953  ramval  13339  ramlb  13350  mrcflem  13794  isacs2  13841  mreacs  13846  acsfn  13847  acsfn1  13849  acsfn2  13851  sscpwex  13978  fpwipodrs  14553  isacs3lem  14555  isacs4lem  14557  isacs5lem  14558  isacs5  14561  oppglsm  15239  lspf  16013  pptbas  17035  clsf  17075  mretopd  17119  neiptopuni  17157  cncls2  17299  cncls  17300  cnntr  17301  restcnrm  17388  cncmp  17417  tgcmp  17426  uncmp  17428  sscmp  17430  hauscmplem  17431  cmpfi  17433  1stcrest  17477  dis2ndc  17484  lly1stc  17520  dislly  17521  kgentopon  17531  kgen2ss  17548  kgencn  17549  kgencn2  17550  kgencn3  17551  txcmplem2  17635  txcmp  17636  tx1stc  17643  txkgen  17645  xkopt  17648  xkococnlem  17652  xkococn  17653  tgqtop  17705  kqnrmlem1  17736  kqnrmlem2  17737  hmphdis  17789  isfil2  17849  isfild  17851  fbasfip  17861  neifil  17873  trfil2  17880  isufil2  17901  trufil  17903  fixufil  17915  cfinufil  17921  fin1aufil  17925  fclscmp  18023  alexsubALTlem2  18040  alexsubALTlem3  18041  alexsubALTlem4  18042  ptcmplem5  18048  tgpconcompeqg  18102  imasf1oxms  18480  met2ndc  18514  zdis  18808  icccmp  18817  ovolf  19339  ismbl2  19384  cmmbl  19390  nulmbl  19391  nulmbl2  19392  unmbl  19393  shftmbl  19394  voliunlem2  19406  ioombl1  19417  uniioombl  19442  sqff1o  20926  musum  20937  usgrares1  21385  esumcst  24416  esumfsup  24421  dmvlsiga  24473  pwsiga  24474  sigaclci  24476  sigainb  24480  insiga  24481  measinb  24536  measres  24537  cntmeas  24541  volmeas  24548  dya2iocucvr  24595  sxbrsigalem1  24596  coinflippv  24702  kur14  24863  conpcon  24883  cvmsi  24913  onsucsuccmpi  26105  limsucncmpi  26107  ismblfin  26154  comppfsc  26285  neibastop1  26286  neibastop2lem  26287  neibastop3  26289  cover2  26313  sstotbnd3  26383  heibor1  26417  heibor  26428  elrfi  26646  cmpfiiin  26649  ismrcd2  26651  isnacs3  26662  aomclem2  27028  islssfg  27044  lmhmfgsplit  27060  lnrfg  27199  pmtrfrn  27276  acsfn1p  27383  stoweidlem57  27681  uhgraedgrnv  28040  sspwtr  28652  sspwtrALT  28653  sspwtrALT2  28654  pwtrVD  28655  pwtrrVD  28656  sspwimp  28748  sspwimpVD  28749  sspwimpcf  28750  sspwimpcfVD  28751  sspwimpALT  28755  sspwimpALT2  28759  pclvalN  30384  pclfinN  30394  pclcmpatN  30395  dochfN  31851
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-in 3295  df-ss 3302  df-pw 3769
  Copyright terms: Public domain W3C validator