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

Theorem elpwi 4547
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 4541 . 2 (𝐴 ∈ 𝒫 𝐵 → (𝐴 ∈ 𝒫 𝐵𝐴𝐵))
21ibi 268 1 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wss 3933  𝒫 cpw 4535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-in 3940  df-ss 3949  df-pw 4537
This theorem is referenced by:  elpwid  4549  elelpwi  4550  elpwunsn  4613  elpw2g  5238  f1opw2  7389  eldifpw  7479  pwuncl  7481  iunpw  7482  f1opwfi  8816  fi0  8872  marypha1lem  8885  marypha1  8886  marypha2  8891  brwdom2  9025  brwdom3  9034  r1pwss  9201  rankpwi  9240  acndom  9465  acnnum  9466  dfac12r  9560  ackbij2lem1  9629  ackbij1lem6  9635  ackbij1b  9649  isfin2-2  9729  ssfin2  9730  enfin2i  9731  compsscnvlem  9780  compssiso  9784  fin11a  9793  enfin1ai  9794  fin12  9823  fin1a2s  9824  fin1a2  9825  hsmexlem2  9837  tskwe2  10183  inttsk  10184  inatsk  10188  hashbclem  13798  pr2pwpr  13825  elss2prb  13833  qshash  15170  incexclem  15179  incexc  15180  incexc2  15181  rpnnen2lem12  15566  smupf  15815  ramval  16332  ramlb  16343  mrcflem  16865  isacs2  16912  mreacs  16917  acsfn  16918  acsfn1  16920  acsfn2  16922  sscpwex  17073  isacs3lem  17764  isacs4lem  17766  isacs5lem  17767  isacs5  17770  pmtrfrn  18515  oppglsm  18696  acsfn1p  19507  lspf  19675  pptbas  21544  clsf  21584  mretopd  21628  neiptopuni  21666  cncls2  21809  cncls  21810  cnntr  21811  restcnrm  21898  cncmp  21928  tgcmp  21937  uncmp  21939  sscmp  21941  hauscmplem  21942  cmpfi  21944  1stcrest  21989  dis2ndc  21996  lly1stc  22032  dislly  22033  comppfsc  22068  kgentopon  22074  kgen2ss  22091  kgencn  22092  kgencn2  22093  kgencn3  22094  txcmplem2  22178  txcmp  22179  tx1stc  22186  txkgen  22188  xkopt  22191  xkococnlem  22195  xkococn  22196  kqnrmlem1  22279  kqnrmlem2  22280  hmphdis  22332  isfil2  22392  isfild  22394  fbasfip  22404  neifil  22416  trfil2  22423  trufil  22446  fixufil  22458  cfinufil  22464  fin1aufil  22468  fclscmp  22566  alexsubALTlem2  22584  alexsubALTlem3  22585  alexsubALTlem4  22586  ptcmplem5  22592  tgpconncompeqg  22647  imasf1oxms  23026  met2ndc  23060  zdis  23351  icccmp  23360  ovolf  24010  ismbl2  24055  cmmbl  24062  nulmbl  24063  nulmbl2  24064  unmbl  24065  shftmbl  24066  voliunlem2  24079  ioombl1  24090  uniioombl  24117  sqff1o  25686  musum  25695  eengtrkg  26699  edgssv2  26907  upgrreslem  27013  umgrreslem  27014  umgrres1lem  27019  upgrres1  27022  uhgrvd00  27243  rabfodom  30193  elpwincl1  30213  fpwrelmap  30395  cmpcref  31013  pcmplfinf  31024  esumcst  31221  esumfsup  31228  esum2d  31251  dmvlsiga  31287  pwsiga  31288  sigaclci  31290  sigainb  31294  insiga  31295  pwldsys  31315  ldgenpisyslem1  31321  ldgenpisyslem3  31323  measinb  31379  measres  31380  cntmeas  31384  volmeas  31389  ddemeas  31394  dya2iocucvr  31441  sxbrsigalem1  31442  omscl  31452  omsf  31453  omsmon  31455  baselcarsg  31463  difelcarsg  31467  carsgsiga  31479  omsmeas  31480  coinflippv  31640  kur14  32360  connpconn  32379  cvmsi  32409  nulsslt  33159  nulssgt  33160  neibastop1  33604  neibastop2lem  33605  neibastop3  33607  onsucsuccmpi  33688  limsucncmpi  33690  bj-elpwg  34239  bj-0int  34287  bj-ismooredr  34295  lindsdom  34767  ismblfin  34814  cover2  34870  sstotbnd3  34935  heibor1  34969  heibor  34980  pclvalN  36906  pclfinN  36916  pclcmpatN  36917  dochfN  38372  elrfi  39169  cmpfiiin  39172  ismrcd2  39174  isnacs3  39185  aomclem2  39533  islssfg  39548  lmhmfgsplit  39564  lnrfg  39597  rfovcnvf1od  40228  dssmapnvod  40244  neik0pk1imk0  40275  isotone2  40277  ntrclsneine0lem  40292  ntrclsiso  40295  ntrclsk2  40296  ntrclskb  40297  ntrclsk3  40298  ntrclsk13  40299  ntrclsk4  40300  ntrneix2  40321  ntrneik13  40326  ntrrn  40350  dssmapntrcls  40356  sspwtr  41032  sspwtrALT  41033  sspwtrALT2  41034  pwtrVD  41035  pwtrrVD  41036  sspwimp  41129  sspwimpVD  41130  sspwimpcf  41131  sspwimpcfVD  41132  sspwimpALT  41136  sspwimpALT2  41139  pwssfi  41184  ssnnf1octb  41332  dvdmsscn  42097  dvnmptconst  42102  dvnxpaek  42103  dvnmul  42104  dvnprodlem3  42109  ismbl3  42148  ismbl4  42155  stoweidlem57  42219  pwsal  42477  prsal  42480  intsal  42490  salexct  42494  issalnnd  42505  sge0rnre  42523  sge0tsms  42539  sge0cl  42540  sge0fsum  42546  sge0sup  42550  sge0less  42551  sge0gerp  42554  sge0resplit  42565  sge0split  42568  nnfoctbdj  42615  ismeannd  42626  psmeasure  42630  caragen0  42665  caragenunidm  42667  caragenuncl  42672  caragendifcl  42673  omeiunle  42676  carageniuncl  42682  caragensal  42684  caratheodorylem2  42686  0ome  42688  isomennd  42690  caragenel2d  42691  caragencmpl  42694  ovnf  42722  ovn02  42727  ovnsubaddlem1  42729  ovnsubaddlem2  42730  ovnsubadd  42731  hspmbl  42788  isvonmbl  42797  vonmblss2  42801  ovnsubadd2lem  42804  vonvolmbl  42820  nsssmfmbf  42932  smfresal  42940  smfpimbor1lem2  42951  sprsymrelfv  43533  prpair  43540  isomuspgrlem2c  43872  lincdifsn  44407  lcosslsp  44421  lindslinindsimp1  44440  lincresunit3lem1  44462  lincresunit3lem2  44463  lincresunit3  44464  elpglem1  44741  aacllem  44830
  Copyright terms: Public domain W3C validator