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

Theorem elpwi 4509
Description: Subset relation implied by membership in a power class. (Contributed by NM, 17-Feb-2007.)
Assertion
Ref Expression
elpwi (𝐴 ∈ 𝒫 𝐵𝐴𝐵)

Proof of Theorem elpwi
StepHypRef Expression
1 elpwg 4503 . 2 (𝐴 ∈ 𝒫 𝐵 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
21ibi 270 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  wss 3884  𝒫 cpw 4500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-pw 4502
This theorem is referenced by:  elpwid  4511  elelpwi  4512  elpwunsn  4584  elpw2g  5214  f1opw2  7384  eldifpw  7474  pwuncl  7476  iunpw  7477  f1opwfi  8816  fi0  8872  marypha1lem  8885  marypha1  8886  marypha2  8891  brwdom2  9025  brwdom3  9034  r1pwss  9201  rankpwi  9240  acndom  9466  acnnum  9467  dfac12r  9561  ackbij2lem1  9634  ackbij1lem6  9640  ackbij1b  9654  isfin2-2  9734  ssfin2  9735  enfin2i  9736  compsscnvlem  9785  compssiso  9789  fin11a  9798  enfin1ai  9799  fin12  9828  fin1a2s  9829  fin1a2  9830  hsmexlem2  9842  tskwe2  10188  inttsk  10189  inatsk  10193  hashbclem  13810  pr2pwpr  13837  elss2prb  13845  qshash  15177  incexclem  15186  incexc  15187  incexc2  15188  rpnnen2lem12  15573  smupf  15820  ramval  16337  ramlb  16348  mrcflem  16872  isacs2  16919  mreacs  16924  acsfn  16925  acsfn1  16927  acsfn2  16929  sscpwex  17080  isacs3lem  17771  isacs4lem  17773  isacs5lem  17774  isacs5  17777  pmtrfrn  18581  oppglsm  18762  acsfn1p  19574  lspf  19742  pptbas  21616  clsf  21656  mretopd  21700  neiptopuni  21738  cncls2  21881  cncls  21882  cnntr  21883  restcnrm  21970  cncmp  22000  tgcmp  22009  uncmp  22011  sscmp  22013  hauscmplem  22014  cmpfi  22016  1stcrest  22061  dis2ndc  22068  lly1stc  22104  dislly  22105  comppfsc  22140  kgentopon  22146  kgen2ss  22163  kgencn  22164  kgencn2  22165  kgencn3  22166  txcmplem2  22250  txcmp  22251  tx1stc  22258  txkgen  22260  xkopt  22263  xkococnlem  22267  xkococn  22268  kqnrmlem1  22351  kqnrmlem2  22352  hmphdis  22404  isfil2  22464  isfild  22466  fbasfip  22476  neifil  22488  trfil2  22495  trufil  22518  fixufil  22530  cfinufil  22536  fin1aufil  22540  fclscmp  22638  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  ptcmplem5  22664  tgpconncompeqg  22720  imasf1oxms  23099  met2ndc  23133  zdis  23424  icccmp  23433  ovolf  24089  ismbl2  24134  cmmbl  24141  nulmbl  24142  nulmbl2  24143  unmbl  24144  shftmbl  24145  voliunlem2  24158  ioombl1  24169  uniioombl  24196  sqff1o  25770  musum  25779  eengtrkg  26783  edgssv2  26991  upgrreslem  27097  umgrreslem  27098  umgrres1lem  27103  upgrres1  27106  uhgrvd00  27327  rabfodom  30277  elpwincl1  30301  fpwrelmap  30498  cmpcref  31203  pcmplfinf  31214  zarclsint  31225  zarcls  31227  esumcst  31430  esumfsup  31437  esum2d  31460  dmvlsiga  31496  pwsiga  31497  sigaclci  31499  sigainb  31503  insiga  31504  pwldsys  31524  ldgenpisyslem1  31530  ldgenpisyslem3  31532  measinb  31588  measres  31589  cntmeas  31593  volmeas  31598  ddemeas  31603  dya2iocucvr  31650  sxbrsigalem1  31651  omscl  31661  omsf  31662  omsmon  31664  baselcarsg  31672  difelcarsg  31676  carsgsiga  31688  omsmeas  31689  coinflippv  31849  kur14  32571  connpconn  32590  cvmsi  32620  nulsslt  33370  nulssgt  33371  neibastop1  33815  neibastop2lem  33816  neibastop3  33818  onsucsuccmpi  33899  limsucncmpi  33901  bj-elpwg  34464  bj-0int  34511  bj-ismooredr  34519  lindsdom  35044  ismblfin  35091  cover2  35145  sstotbnd3  35207  heibor1  35241  heibor  35252  pclvalN  37179  pclfinN  37189  pclcmpatN  37190  dochfN  38645  elrfi  39622  cmpfiiin  39625  ismrcd2  39627  isnacs3  39638  aomclem2  39986  islssfg  40001  lmhmfgsplit  40017  lnrfg  40050  rfovcnvf1od  40692  dssmapnvod  40708  neik0pk1imk0  40737  isotone2  40739  ntrclsneine0lem  40754  ntrclsiso  40757  ntrclsk2  40758  ntrclskb  40759  ntrclsk3  40760  ntrclsk13  40761  ntrclsk4  40762  ntrneix2  40783  ntrneik13  40788  ntrrn  40812  dssmapntrcls  40818  sspwtr  41514  sspwtrALT  41515  sspwtrALT2  41516  pwtrVD  41517  pwtrrVD  41518  sspwimp  41611  sspwimpVD  41612  sspwimpcf  41613  sspwimpcfVD  41614  sspwimpALT  41618  sspwimpALT2  41621  pwssfi  41666  ssnnf1octb  41809  dvdmsscn  42565  dvnmptconst  42570  dvnxpaek  42571  dvnmul  42572  dvnprodlem3  42577  ismbl3  42615  ismbl4  42622  stoweidlem57  42686  pwsal  42944  prsal  42947  intsal  42957  salexct  42961  issalnnd  42972  sge0rnre  42990  sge0tsms  43006  sge0cl  43007  sge0fsum  43013  sge0sup  43017  sge0less  43018  sge0gerp  43021  sge0resplit  43032  sge0split  43035  nnfoctbdj  43082  ismeannd  43093  psmeasure  43097  caragen0  43132  caragenunidm  43134  caragenuncl  43139  caragendifcl  43140  omeiunle  43143  carageniuncl  43149  caragensal  43151  caratheodorylem2  43153  0ome  43155  isomennd  43157  caragenel2d  43158  caragencmpl  43161  ovnf  43189  ovn02  43194  ovnsubaddlem1  43196  ovnsubaddlem2  43197  ovnsubadd  43198  hspmbl  43255  isvonmbl  43264  vonmblss2  43268  ovnsubadd2lem  43271  vonvolmbl  43287  nsssmfmbf  43399  smfresal  43407  smfpimbor1lem2  43418  sprsymrelfv  43998  prpair  44005  isomuspgrlem2c  44335  lincdifsn  44820  lcosslsp  44834  lindslinindsimp1  44853  lincresunit3lem1  44875  lincresunit3lem2  44876  lincresunit3  44877  elpglem1  45227  aacllem  45316
  Copyright terms: Public domain W3C validator