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

Theorem elpwid 4556
Description: An element of a power class is a subclass. Deduction form of elpwi 4554. (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 4554 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wss 3940  𝒫 cpw 4542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-in 3947  df-ss 3956  df-pw 4544
This theorem is referenced by:  fopwdom  8614  ssenen  8680  fival  8865  dffi2  8876  elfiun  8883  tskwe  9368  acndom2  9469  fodomfi2  9475  infpwfien  9477  dfac12lem2  9559  ackbij1lem9  9639  ackbij1lem10  9640  ackbij1lem11  9641  ackbij1lem16  9646  ackbij2lem3  9652  cfss  9676  fin23lem7  9727  fin23lem11  9728  enfin2i  9732  isf32lem8  9771  isf34lem4  9788  isf34lem7  9790  isf34lem6  9791  isfin1-3  9797  fin1a2lem13  9823  ttukeylem6  9925  uzssz  12253  elfzoelz  13028  ackbijnn  15173  incexclem  15181  smuval2  15821  smupvallem  15822  smueqlem  15829  ramub1lem1  16352  ramub1lem2  16353  restid2  16694  mress  16854  mrcuni  16882  mreexexlem4d  16908  mreexexd  16909  mreexdomd  16910  isacs2  16914  acsfn  16920  isdrs2  17539  ipodrsima  17765  isacs3lem  17766  acsfiindd  17777  lagsubg2  18271  cntzrcl  18387  sylow1lem2  18644  sylow1lem3  18645  sylow1lem4  18646  sylow2alem2  18663  sylow2a  18664  lsmpropd  18723  lssacs  19659  lssacsex  19836  lbsextlem2  19851  lbsextlem3  19852  lbsextlem4  19853  elocv  20731  ppttop  21534  epttop  21536  clsval2  21577  mretopd  21619  neiss2  21628  neiptopnei  21659  ordtbas  21719  subbascn  21781  discmp  21925  uncmp  21930  conncompconn  21959  1stcfb  21972  2ndcdisj  21983  restnlly  22009  nllyrest  22013  nllyidm  22016  cldllycmp  22022  1stckgenlem  22080  dfac14  22145  xkoccn  22146  txnlly  22164  txkgen  22179  xkopt  22182  xkoco2cn  22185  xkoinjcn  22214  tgqtop  22239  nrmhmph  22321  fbelss  22360  fbssfi  22364  infil  22390  alexsubALTlem3  22576  alexsubALTlem4  22577  ustssxp  22731  trust  22756  utopsnneiplem  22774  blssm  22946  blin2  22957  metustss  23079  metust  23086  psmetutop  23095  restmetu  23098  icccmplem2  23349  cncfrss  23417  cncfrss2  23418  bndth  23480  lebnum  23486  ovolicc2  24041  vitalilem5  24131  i1fd  24200  dvbsss  24418  perfdvf  24419  plybss  24702  wilthlem2  25563  f1otrg  26574  uhgrss  26766  upgrss  26790  usgrss  26876  eupth2lems  27934  ubthlem1  28564  elpwdifcl  30204  elpwiuncl  30205  ssnnssfz  30426  trsp2cyc  30682  indf1ofs  31174  esumval  31194  esumel  31195  gsumesum  31207  esumlub  31208  esumpcvgval  31226  esumcvg  31234  elsigass  31273  ispisys2  31301  sigapildsyslem  31309  sigapildsys  31310  ldgenpisyslem1  31311  ldgenpisys  31314  dynkin  31315  rossspw  31317  srossspw  31324  ddemeas  31384  br2base  31416  sxbrsigalem0  31418  dya2iocucvr  31431  sxbrsigalem2  31433  sxbrsiga  31437  oms0  31444  omssubadd  31447  carsguni  31455  elcarsgss  31456  carsggect  31465  omsmeas  31470  eulerpartlemgvv  31523  coinfliplem  31625  ballotlemfmpn  31641  cvmliftmolem2  32416  cvmlift3lem8  32460  neibastop1  33594  neibastop2lem  33595  neibastop2  33596  filnetlem4  33616  cnambfre  34810  heiborlem3  34962  heiborlem5  34964  heiborlem6  34965  heiborlem10  34969  heibor  34970  mapd1o  38654  elrfi  39159  elrfirn  39160  elrfirn2  39161  ismrcd1  39163  istopclsd  39165  mrefg3  39173  aomclem2  39523  lsmfgcl  39542  lmhmfgima  39552  elmnc  39604  rfovcnvf1od  40218  rfovcnvfvd  40221  fsovrfovd  40223  fsovcnvlem  40227  dssmapnvod  40234  ntrk0kbimka  40257  clsk3nimkb  40258  neik0pk1imk0  40265  ntrclsfveq1  40278  ntrclsfveq2  40279  ntrclsfveq  40280  ntrclsss  40281  ntrclsiso  40285  ntrclsk2  40286  ntrclskb  40287  ntrclsk3  40288  ntrclsk13  40289  ntrclsk4  40290  ntrneifv3  40300  ntrneineine0lem  40301  ntrneineine1lem  40302  ntrneifv4  40303  ntrneiel2  40304  ntrneicls00  40307  ntrneicls11  40308  ntrneiiso  40309  ntrneik2  40310  ntrneikb  40312  ntrneixb  40313  ntrneik3  40314  ntrneix3  40315  ntrneik13  40316  ntrneix13  40317  ntrneik4w  40318  clsneiel2  40327  clsneifv3  40328  clsneifv4  40329  neicvgel2  40338  neicvgfv  40339  gneispb  40349  elpwinss  41179  stoweidlem39  42193  stoweidlem50  42204  sge0resrnlem  42554  sge0iunmptlemre  42566  psmeasurelem  42621  psmeasure  42622  ssnn0ssfz  44232
  Copyright terms: Public domain W3C validator