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

Theorem elpwid 4118
Description: An element of a power class is a subclass. Deduction form of elpwi 4117. (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 4117 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  wss 3540  𝒫 cpw 4108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110
This theorem is referenced by:  fopwdom  7931  ssenen  7997  fival  8179  dffi2  8190  elfiun  8197  tskwe  8637  acndom2  8738  fodomfi2  8744  infpwfien  8746  dfac12lem2  8827  ackbij1lem9  8911  ackbij1lem10  8912  ackbij1lem11  8913  ackbij1lem16  8918  ackbij2lem3  8924  cfss  8948  fin23lem7  8999  fin23lem11  9000  enfin2i  9004  isf32lem8  9043  isf34lem4  9060  isf34lem7  9062  isf34lem6  9063  isfin1-3  9069  fin1a2lem13  9095  ttukeylem6  9197  uzssz  11542  elfzoelz  12297  ackbijnn  14348  incexclem  14356  smuval2  14991  smupvallem  14992  smueqlem  14999  ramub1lem1  15517  ramub1lem2  15518  restid2  15863  mress  16025  mrcuni  16053  mreexexlem4d  16079  mreexexd  16080  mreexexdOLD  16081  mreexdomd  16082  acsfn  16092  isdrs2  16711  ipodrsima  16937  isacs3lem  16938  acsfiindd  16949  lagsubg2  17427  cntzrcl  17532  sylow1lem2  17786  sylow1lem3  17787  sylow1lem4  17788  sylow2alem2  17805  sylow2a  17806  lsmpropd  17862  lssacs  18737  lssacsex  18914  lbsextlem2  18929  lbsextlem3  18930  lbsextlem4  18931  elocv  19779  ppttop  20569  epttop  20571  clsval2  20612  mretopd  20654  neiss2  20663  neiptopnei  20694  ordtbas  20754  subbascn  20816  discmp  20959  uncmp  20964  concompcon  20993  1stcfb  21006  2ndcdisj  21017  restnlly  21043  nllyrest  21047  nllyidm  21050  cldllycmp  21056  1stckgenlem  21114  dfac14  21179  xkoccn  21180  txnlly  21198  txkgen  21213  xkopt  21216  xkoco2cn  21219  xkoinjcn  21248  tgqtop  21273  nrmhmph  21355  fbelss  21395  fbssfi  21399  infil  21425  alexsubALTlem3  21611  alexsubALTlem4  21612  ustssxp  21766  trust  21791  utopsnneiplem  21809  blssm  21981  blin2  21992  metustss  22114  metustfbas  22120  metust  22121  psmetutop  22130  restmetu  22133  icccmplem2  22382  cncfrss  22450  cncfrss2  22451  bndth  22513  lebnum  22519  ovolicc2  23042  vitalilem5  23132  i1fd  23199  dvbsss  23417  perfdvf  23418  plybss  23699  wilthlem2  24540  f1otrg  25497  uhgrass  25629  umgrass  25642  usgrass  25684  eupath2  26301  ubthlem1  26904  elpwdifcl  28536  elpwiuncl  28537  ssnnssfz  28731  indf1ofs  29209  esumval  29229  esumel  29230  gsumesum  29242  esumlub  29243  esumpcvgval  29261  esumcvg  29269  elsigass  29309  ispisys2  29337  sigapildsyslem  29345  sigapildsys  29346  ldgenpisyslem1  29347  ldgenpisys  29350  dynkin  29351  rossspw  29353  srossspw  29360  ddemeas  29420  br2base  29452  sxbrsigalem0  29454  dya2iocucvr  29467  sxbrsigalem2  29469  sxbrsiga  29473  oms0  29480  omssubadd  29483  carsguni  29491  elcarsgss  29492  carsggect  29501  omsmeas  29506  eulerpartlemgvv  29559  coinfliplem  29661  ballotlemfmpn  29677  cvmliftmolem2  30312  cvmlift3lem8  30356  neibastop1  31318  neibastop2lem  31319  neibastop2  31320  filnetlem4  31340  cnambfre  32422  heiborlem3  32576  heiborlem5  32578  heiborlem6  32579  heiborlem10  32583  heibor  32584  mapd1o  35749  elrfi  36069  elrfirn  36070  elrfirn2  36071  ismrcd1  36073  istopclsd  36075  mrefg3  36083  aomclem2  36437  lsmfgcl  36456  lmhmfgima  36466  elmnc  36519  rfovcnvf1od  37112  rfovcnvfvd  37115  fsovrfovd  37117  fsovcnvlem  37121  dssmapnvod  37128  ntrk0kbimka  37151  clsk3nimkb  37152  neik0pk1imk0  37159  ntrclsfveq1  37172  ntrclsfveq2  37173  ntrclsfveq  37174  ntrclsss  37175  ntrclsiso  37179  ntrclsk2  37180  ntrclskb  37181  ntrclsk3  37182  ntrclsk13  37183  ntrclsk4  37184  ntrneifv3  37194  ntrneineine0lem  37195  ntrneineine1lem  37196  ntrneifv4  37197  ntrneiel2  37198  ntrneicls00  37201  ntrneicls11  37202  ntrneiiso  37203  ntrneik2  37204  ntrneikb  37206  ntrneixb  37207  ntrneik3  37208  ntrneix3  37209  ntrneik13  37210  ntrneix13  37211  ntrneik4w  37212  clsneiel2  37221  clsneifv3  37222  clsneifv4  37223  neicvgel2  37232  neicvgfv  37233  gneispb  37243  stoweidlem39  38726  stoweidlem50  38737  sge0resrnlem  39090  sge0iunmptlemre  39102  psmeasurelem  39157  psmeasure  39158  uhgrss  40278  upgrss  40306  usgrss  40396  eupth2lems  41398  ssnn0ssfz  41912
  Copyright terms: Public domain W3C validator