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

Theorem elpwi 4019
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 4018 . 2  |-  ( A  e.  ~P B  -> 
( A  e.  ~P B 
<->  A  C_  B )
)
21ibi 241 1  |-  ( A  e.  ~P B  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767    C_ wss 3476   ~Pcpw 4010
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-pw 4012
This theorem is referenced by:  elpwid  4020  elelpwi  4021  elpwunsn  4068  elpw2g  4610  f1opw2  6510  eldifpw  6590  iunpw  6592  f1opwfi  7820  fi0  7876  fiin  7878  marypha1lem  7889  marypha1  7890  marypha2  7895  brwdom2  7995  brwdom3  8004  r1pwss  8198  rankpwi  8237  acndom  8428  acnnum  8429  dfac12r  8522  ackbij2lem1  8595  ackbij1lem6  8601  ackbij1b  8615  isfin2-2  8695  ssfin2  8696  enfin2i  8697  compsscnvlem  8746  compssiso  8750  fin11a  8759  enfin1ai  8760  fin12  8789  fin1a2s  8790  fin1a2  8791  hsmexlem2  8803  tskwe2  9147  inttsk  9148  inatsk  9152  hashbclem  12463  pr2pwpr  12482  qshash  13598  incexclem  13607  incexc  13608  incexc2  13609  rpnnen2  13816  smupf  13983  ramval  14381  ramlb  14392  mrcflem  14857  isacs2  14904  mreacs  14909  acsfn  14910  acsfn1  14912  acsfn2  14914  sscpwex  15041  fpwipodrs  15647  isacs3lem  15649  isacs4lem  15651  isacs5lem  15652  isacs5  15655  pmtrfrn  16279  oppglsm  16458  lspf  17403  pptbas  19275  clsf  19315  mretopd  19359  neiptopuni  19397  cncls2  19540  cncls  19541  cnntr  19542  restcnrm  19629  cncmp  19658  tgcmp  19667  uncmp  19669  sscmp  19671  hauscmplem  19672  cmpfi  19674  1stcrest  19720  dis2ndc  19727  lly1stc  19763  dislly  19764  kgentopon  19774  kgen2ss  19791  kgencn  19792  kgencn2  19793  kgencn3  19794  txcmplem2  19878  txcmp  19879  tx1stc  19886  txkgen  19888  xkopt  19891  xkococnlem  19895  xkococn  19896  tgqtop  19948  kqnrmlem1  19979  kqnrmlem2  19980  hmphdis  20032  isfil2  20092  isfild  20094  fbasfip  20104  neifil  20116  trfil2  20123  isufil2  20144  trufil  20146  fixufil  20158  cfinufil  20164  fin1aufil  20168  fclscmp  20266  alexsubALTlem2  20283  alexsubALTlem3  20284  alexsubALTlem4  20285  ptcmplem5  20291  tgpconcompeqg  20345  imasf1oxms  20727  met2ndc  20761  zdis  21056  icccmp  21065  ovolf  21628  ismbl2  21673  cmmbl  21680  nulmbl  21681  nulmbl2  21682  unmbl  21683  shftmbl  21684  voliunlem2  21696  ioombl1  21707  uniioombl  21733  sqff1o  23184  musum  23195  f1otrg  23850  eengtrkg  23964  usgrares1  24086  esumcst  27711  esumfsup  27716  dmvlsiga  27769  pwsiga  27770  sigaclci  27772  sigainb  27776  insiga  27777  measinb  27832  measres  27833  cntmeas  27837  volmeas  27843  ddemeas  27848  dya2iocucvr  27895  sxbrsigalem1  27896  oms0  27906  omsmon  27907  coinflippv  28062  kur14  28300  conpcon  28320  cvmsi  28350  onsucsuccmpi  29485  limsucncmpi  29487  ismblfin  29632  comppfsc  29779  neibastop1  29780  neibastop2lem  29781  neibastop3  29783  cover2  29807  sstotbnd3  29875  heibor1  29909  heibor  29920  elrfi  30230  cmpfiiin  30233  ismrcd2  30235  isnacs3  30246  aomclem2  30605  islssfg  30620  lmhmfgsplit  30636  lnrfg  30672  acsfn1p  30753  stoweidlem57  31357  uhgraedgrnv  31818  edgssv2ALT  31870  edgssv2  31871  lincdifsn  32098  lcosslsp  32112  lindslinindsimp1  32131  lincresunit3lem1  32153  lincresunit3lem2  32154  lincresunit3  32155  sspwtr  32699  sspwtrALT  32700  sspwtrALT2  32703  pwtrVD  32704  pwtrrVD  32705  sspwimp  32798  sspwimpVD  32799  sspwimpcf  32800  sspwimpcfVD  32801  sspwimpALT  32805  sspwimpALT2  32808  pclvalN  34686  pclfinN  34696  pclcmpatN  34697  dochfN  36153
  Copyright terms: Public domain W3C validator