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  7953  ssenen  8019  fival  8201  dffi2  8212  elfiun  8219  tskwe  8659  acndom2  8760  fodomfi2  8766  infpwfien  8768  dfac12lem2  8849  ackbij1lem9  8933  ackbij1lem10  8934  ackbij1lem11  8935  ackbij1lem16  8940  ackbij2lem3  8946  cfss  8970  fin23lem7  9021  fin23lem11  9022  enfin2i  9026  isf32lem8  9065  isf34lem4  9082  isf34lem7  9084  isf34lem6  9085  isfin1-3  9091  fin1a2lem13  9117  ttukeylem6  9219  uzssz  11583  elfzoelz  12339  ackbijnn  14399  incexclem  14407  smuval2  15042  smupvallem  15043  smueqlem  15050  ramub1lem1  15568  ramub1lem2  15569  restid2  15914  mress  16076  mrcuni  16104  mreexexlem4d  16130  mreexexd  16131  mreexexdOLD  16132  mreexdomd  16133  acsfn  16143  isdrs2  16762  ipodrsima  16988  isacs3lem  16989  acsfiindd  17000  lagsubg2  17478  cntzrcl  17583  sylow1lem2  17837  sylow1lem3  17838  sylow1lem4  17839  sylow2alem2  17856  sylow2a  17857  lsmpropd  17913  lssacs  18788  lssacsex  18965  lbsextlem2  18980  lbsextlem3  18981  lbsextlem4  18982  elocv  19831  ppttop  20621  epttop  20623  clsval2  20664  mretopd  20706  neiss2  20715  neiptopnei  20746  ordtbas  20806  subbascn  20868  discmp  21011  uncmp  21016  concompcon  21045  1stcfb  21058  2ndcdisj  21069  restnlly  21095  nllyrest  21099  nllyidm  21102  cldllycmp  21108  1stckgenlem  21166  dfac14  21231  xkoccn  21232  txnlly  21250  txkgen  21265  xkopt  21268  xkoco2cn  21271  xkoinjcn  21300  tgqtop  21325  nrmhmph  21407  fbelss  21447  fbssfi  21451  infil  21477  alexsubALTlem3  21663  alexsubALTlem4  21664  ustssxp  21818  trust  21843  utopsnneiplem  21861  blssm  22033  blin2  22044  metustss  22166  metustfbas  22172  metust  22173  psmetutop  22182  restmetu  22185  icccmplem2  22434  cncfrss  22502  cncfrss2  22503  bndth  22565  lebnum  22571  ovolicc2  23097  vitalilem5  23187  i1fd  23254  dvbsss  23472  perfdvf  23473  plybss  23754  wilthlem2  24595  f1otrg  25551  uhgrss  25730  upgrss  25755  uhgrass  25835  umgrass  25848  usgrass  25890  eupath2  26507  ubthlem1  27110  elpwdifcl  28742  elpwiuncl  28743  ssnnssfz  28937  indf1ofs  29415  esumval  29435  esumel  29436  gsumesum  29448  esumlub  29449  esumpcvgval  29467  esumcvg  29475  elsigass  29515  ispisys2  29543  sigapildsyslem  29551  sigapildsys  29552  ldgenpisyslem1  29553  ldgenpisys  29556  dynkin  29557  rossspw  29559  srossspw  29566  ddemeas  29626  br2base  29658  sxbrsigalem0  29660  dya2iocucvr  29673  sxbrsigalem2  29675  sxbrsiga  29679  oms0  29686  omssubadd  29689  carsguni  29697  elcarsgss  29698  carsggect  29707  omsmeas  29712  eulerpartlemgvv  29765  coinfliplem  29867  ballotlemfmpn  29883  cvmliftmolem2  30518  cvmlift3lem8  30562  neibastop1  31524  neibastop2lem  31525  neibastop2  31526  filnetlem4  31546  cnambfre  32628  heiborlem3  32782  heiborlem5  32784  heiborlem6  32785  heiborlem10  32789  heibor  32790  mapd1o  35955  elrfi  36275  elrfirn  36276  elrfirn2  36277  ismrcd1  36279  istopclsd  36281  mrefg3  36289  aomclem2  36643  lsmfgcl  36662  lmhmfgima  36672  elmnc  36725  rfovcnvf1od  37318  rfovcnvfvd  37321  fsovrfovd  37323  fsovcnvlem  37327  dssmapnvod  37334  ntrk0kbimka  37357  clsk3nimkb  37358  neik0pk1imk0  37365  ntrclsfveq1  37378  ntrclsfveq2  37379  ntrclsfveq  37380  ntrclsss  37381  ntrclsiso  37385  ntrclsk2  37386  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  ntrclsk4  37390  ntrneifv3  37400  ntrneineine0lem  37401  ntrneineine1lem  37402  ntrneifv4  37403  ntrneiel2  37404  ntrneicls00  37407  ntrneicls11  37408  ntrneiiso  37409  ntrneik2  37410  ntrneikb  37412  ntrneixb  37413  ntrneik3  37414  ntrneix3  37415  ntrneik13  37416  ntrneix13  37417  ntrneik4w  37418  clsneiel2  37427  clsneifv3  37428  clsneifv4  37429  neicvgel2  37438  neicvgfv  37439  gneispb  37449  stoweidlem39  38932  stoweidlem50  38943  sge0resrnlem  39296  sge0iunmptlemre  39308  psmeasurelem  39363  psmeasure  39364  usgrss  40404  eupth2lems  41406  ssnn0ssfz  41920
  Copyright terms: Public domain W3C validator