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

Theorem elpwid 4573
Description: An element of a power class is a subclass. Deduction form of elpwi 4571. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
elpwid.1 (𝜑𝐴 ∈ 𝒫 𝐵)
Assertion
Ref Expression
elpwid (𝜑𝐴𝐵)

Proof of Theorem elpwid
StepHypRef Expression
1 elpwid.1 . 2 (𝜑𝐴 ∈ 𝒫 𝐵)
2 elpwi 4571 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wss 3914  𝒫 cpw 4564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3449  df-in 3921  df-ss 3931  df-pw 4566
This theorem is referenced by:  cofon1  8622  cofon2  8623  fopwdom  9030  ssenen  9101  fival  9356  dffi2  9367  elfiun  9374  tskwe  9894  acndom2  9998  fodomfi2  10004  infpwfien  10006  dfac12lem2  10088  ackbij1lem9  10172  ackbij1lem10  10173  ackbij1lem11  10174  ackbij1lem16  10179  ackbij2lem3  10185  cfss  10209  fin23lem7  10260  fin23lem11  10261  enfin2i  10265  isf32lem8  10304  isf34lem4  10321  isf34lem7  10323  isf34lem6  10324  isfin1-3  10330  fin1a2lem13  10356  ttukeylem6  10458  uzssz  12792  elfzoelz  13581  ackbijnn  15721  incexclem  15729  smuval2  16370  smupvallem  16371  smueqlem  16378  ramub1lem1  16906  ramub1lem2  16907  restid2  17320  mress  17481  mrcuni  17509  mreexexlem4d  17535  mreexexd  17536  mreexdomd  17537  isacs2  17541  acsfn  17547  isdrs2  18203  ipodrsima  18438  isacs3lem  18439  acsfiindd  18450  lagsubg2  18999  cntzrcl  19115  sylow1lem2  19389  sylow1lem3  19390  sylow1lem4  19391  sylow2alem2  19408  sylow2a  19409  lsmpropd  19467  lssacs  20472  lssacsex  20650  lbsextlem2  20665  lbsextlem3  20666  lbsextlem4  20667  elocv  21095  ppttop  22380  epttop  22382  clsval2  22424  mretopd  22466  neiss2  22475  neiptopnei  22506  ordtbas  22566  subbascn  22628  discmp  22772  uncmp  22777  conncompconn  22806  1stcfb  22819  2ndcdisj  22830  restnlly  22856  nllyrest  22860  nllyidm  22863  cldllycmp  22869  1stckgenlem  22927  dfac14  22992  xkoccn  22993  txnlly  23011  txkgen  23026  xkopt  23029  xkoco2cn  23032  xkoinjcn  23061  tgqtop  23086  nrmhmph  23168  fbelss  23207  fbssfi  23211  infil  23237  alexsubALTlem3  23423  alexsubALTlem4  23424  ustssxp  23579  trust  23604  utopsnneiplem  23622  blssm  23794  blin2  23805  metustss  23930  metust  23937  psmetutop  23946  restmetu  23949  icccmplem2  24209  cncfrss  24277  cncfrss2  24278  bndth  24344  lebnum  24350  ovolicc2  24909  vitalilem5  24999  i1fd  25068  dvbsss  25289  perfdvf  25290  plybss  25578  wilthlem2  26441  oldf  27216  newf  27217  leftf  27224  rightf  27225  elmade  27226  ssltleft  27229  ssltright  27230  cofsslt  27266  coinitsslt  27267  f1otrg  27862  uhgrss  28064  upgrss  28088  usgrss  28174  eupth2lems  29231  ubthlem1  29861  elpwdifcl  31504  elpwiuncl  31505  ssnnssfz  31744  pwrssmgc  31916  trsp2cyc  32028  ghmqusker  32253  zarcmplem  32526  indf1ofs  32689  esumval  32709  esumel  32710  gsumesum  32722  esumlub  32723  esumpcvgval  32741  esumcvg  32749  elsigass  32788  ispisys2  32816  sigapildsyslem  32824  sigapildsys  32825  ldgenpisyslem1  32826  ldgenpisys  32829  dynkin  32830  rossspw  32832  srossspw  32839  ddemeas  32899  br2base  32933  sxbrsigalem0  32935  dya2iocucvr  32948  sxbrsigalem2  32950  sxbrsiga  32954  oms0  32961  omssubadd  32964  carsguni  32972  elcarsgss  32973  carsggect  32982  omsmeas  32987  eulerpartlemgvv  33040  coinfliplem  33142  ballotlemfmpn  33158  cvmliftmolem2  33940  cvmlift3lem8  33984  neibastop1  34884  neibastop2lem  34885  neibastop2  34886  filnetlem4  34906  cnambfre  36176  heiborlem3  36322  heiborlem5  36324  heiborlem6  36325  heiborlem10  36329  heibor  36330  mapd1o  40161  sticksstones3  40606  prjcrv0  41018  elrfi  41064  elrfirn  41065  elrfirn2  41066  ismrcd1  41068  istopclsd  41070  mrefg3  41078  aomclem2  41429  lsmfgcl  41448  lmhmfgima  41458  elmnc  41510  fpwfvss  41776  rfovcnvf1od  42368  rfovcnvfvd  42371  fsovrfovd  42373  fsovcnvlem  42377  dssmapnvod  42384  ntrk0kbimka  42403  clsk3nimkb  42404  neik0pk1imk0  42411  ntrclsfveq1  42424  ntrclsfveq2  42425  ntrclsfveq  42426  ntrclsss  42427  ntrclsiso  42431  ntrclsk2  42432  ntrclskb  42433  ntrclsk3  42434  ntrclsk13  42435  ntrclsk4  42436  ntrneifv3  42446  ntrneineine0lem  42447  ntrneineine1lem  42448  ntrneifv4  42449  ntrneiel2  42450  ntrneicls00  42453  ntrneicls11  42454  ntrneiiso  42455  ntrneik2  42456  ntrneikb  42458  ntrneixb  42459  ntrneik3  42460  ntrneix3  42461  ntrneik13  42462  ntrneix13  42463  ntrneik4w  42464  clsneiel2  42473  clsneifv3  42474  clsneifv4  42475  neicvgel2  42484  neicvgfv  42485  gneispb  42495  elpwinss  43349  stoweidlem39  44370  stoweidlem50  44381  sge0resrnlem  44734  sge0iunmptlemre  44746  psmeasurelem  44801  psmeasure  44802  ssnn0ssfz  46515  iscnrm3rlem3  47065  iscnrm3rlem8  47070  iscnrm3llem1  47072  iscnrm3llem2  47073  iscnrm3l  47074  pgindlem  47250
  Copyright terms: Public domain W3C validator