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

Theorem elpwi 3926
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 3925 . 2  |-  ( A  e.  ~P B  -> 
( A  e.  ~P B 
<->  A  C_  B )
)
21ibi 244 1  |-  ( A  e.  ~P B  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872    C_ wss 3372   ~Pcpw 3917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-v 3018  df-in 3379  df-ss 3386  df-pw 3919
This theorem is referenced by:  elpwid  3927  elelpwi  3928  elpwunsn  3976  elpw2g  4523  f1opw2  6473  eldifpw  6554  iunpw  6556  f1opwfi  7824  fi0  7880  fiin  7882  marypha1lem  7893  marypha1  7894  marypha2  7899  brwdom2  8034  brwdom3  8043  r1pwss  8200  rankpwi  8239  acndom  8426  acnnum  8427  dfac12r  8520  ackbij2lem1  8593  ackbij1lem6  8599  ackbij1b  8613  isfin2-2  8693  ssfin2  8694  enfin2i  8695  compsscnvlem  8744  compssiso  8748  fin11a  8757  enfin1ai  8758  fin12  8787  fin1a2s  8788  fin1a2  8789  hsmexlem2  8801  tskwe2  9142  inttsk  9143  inatsk  9147  hashbclem  12556  pr2pwpr  12577  elss2prb  12584  qshash  13821  incexclem  13830  incexc  13831  incexc2  13832  rpnnen2  14214  smupf  14388  ramval  14896  ramvalOLD  14897  ramlb  14913  mrcflem  15448  isacs2  15495  mreacs  15500  acsfn  15501  acsfn1  15503  acsfn2  15505  sscpwex  15656  fpwipodrs  16346  isacs3lem  16348  isacs4lem  16350  isacs5lem  16351  isacs5  16354  pmtrfrn  17035  oppglsm  17230  lspf  18133  pptbas  19958  clsf  19998  mretopd  20043  neiptopuni  20081  cncls2  20224  cncls  20225  cnntr  20226  restcnrm  20313  cncmp  20342  tgcmp  20351  uncmp  20353  sscmp  20355  hauscmplem  20356  cmpfi  20358  1stcrest  20403  dis2ndc  20410  lly1stc  20446  dislly  20447  comppfsc  20482  kgentopon  20488  kgen2ss  20505  kgencn  20506  kgencn2  20507  kgencn3  20508  txcmplem2  20592  txcmp  20593  tx1stc  20600  txkgen  20602  xkopt  20605  xkococnlem  20609  xkococn  20610  kqnrmlem1  20693  kqnrmlem2  20694  hmphdis  20746  isfil2  20806  isfild  20808  fbasfip  20818  neifil  20830  trfil2  20837  trufil  20860  fixufil  20872  cfinufil  20878  fin1aufil  20882  fclscmp  20980  alexsubALTlem2  20998  alexsubALTlem3  20999  alexsubALTlem4  21000  ptcmplem5  21006  tgpconcompeqg  21061  imasf1oxms  21439  met2ndc  21473  zdis  21769  icccmp  21778  ovolf  22370  ismbl2  22416  cmmbl  22423  nulmbl  22424  nulmbl2  22425  unmbl  22426  shftmbl  22427  voliunlem2  22439  ioombl1  22450  uniioombl  22482  sqff1o  24044  musum  24055  eengtrkg  24950  usgrares1  25073  rabfodom  28076  elpwincl1  28092  fpwrelmap  28261  cmpcref  28622  pcmplfinf  28633  esumcst  28829  esumfsup  28836  esum2d  28859  dmvlsiga  28896  pwsiga  28897  sigaclci  28899  sigainb  28903  insiga  28904  pwldsys  28924  ldgenpisyslem1  28930  ldgenpisyslem3  28932  measinb  28988  measres  28989  cntmeas  28993  volmeas  28999  ddemeas  29004  dya2iocucvr  29051  sxbrsigalem1  29052  omscl  29064  omsf  29065  omsclOLD  29068  omsfOLD  29069  omsmon  29071  oms0OLD  29074  omsmonOLD  29075  baselcarsg  29083  difelcarsg  29087  carsgsiga  29099  omsmeas  29100  omsmeasOLD  29101  coinflippv  29261  kur14  29884  conpcon  29903  cvmsi  29933  neibastop1  30957  neibastop2lem  30958  neibastop3  30960  onsucsuccmpi  31045  limsucncmpi  31047  ismblfin  31882  cover2  31941  sstotbnd3  32009  heibor1  32043  heibor  32054  pclvalN  33361  pclfinN  33371  pclcmpatN  33372  dochfN  34830  elrfi  35442  cmpfiiin  35445  ismrcd2  35447  isnacs3  35458  aomclem2  35820  islssfg  35835  lmhmfgsplit  35851  lnrfg  35885  acsfn1p  35972  sspwtr  37119  sspwtrALT  37120  sspwtrALT2  37129  pwtrVD  37130  pwtrrVD  37131  sspwimp  37225  sspwimpVD  37226  sspwimpcf  37227  sspwimpcfVD  37228  sspwimpALT  37232  sspwimpALT2  37235  pwssfi  37291  elpwinss  37297  ssnnf1octb  37368  dvdmsscn  37688  dvnmptconst  37693  dvnxpaek  37694  dvnmul  37695  dvnprodlem3  37700  stoweidlem57  37795  pwsal  38034  prsal  38037  intsal  38047  sge0rnre  38051  sge0tsms  38067  sge0cl  38068  sge0fsum  38074  sge0sup  38078  sge0less  38079  sge0gerp  38082  sge0resplit  38093  sge0split  38096  nnfoctbdj  38139  ismeannd  38150  psmeasure  38154  caragen0  38172  caragenunidm  38174  caragenuncl  38179  caragendifcl  38180  omeiunle  38183  carageniuncl  38189  caragensal  38191  caratheodorylem2  38193  0ome  38195  isomennd  38197  ovnf  38226  ovn02  38231  ovnsubaddlem1  38233  ovnsubaddlem2  38234  ovnsubadd  38235  edgassv2  39027  umgrres1lem  39108  upgrres1  39111  uhgraedgrnv  39248  edgssv2ALT  39298  edgssv2  39299  lincdifsn  39804  lcosslsp  39818  lindslinindsimp1  39837  lincresunit3lem1  39859  lincresunit3lem2  39860  lincresunit3  39861  aacllem  40127
  Copyright terms: Public domain W3C validator