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

Theorem elpwid 4203
Description: An element of a power class is a subclass. Deduction form of elpwi 4201. (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 4201 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wss 3607  𝒫 cpw 4191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-pw 4193
This theorem is referenced by:  fopwdom  8109  ssenen  8175  fival  8359  dffi2  8370  elfiun  8377  tskwe  8814  acndom2  8915  fodomfi2  8921  infpwfien  8923  dfac12lem2  9004  ackbij1lem9  9088  ackbij1lem10  9089  ackbij1lem11  9090  ackbij1lem16  9095  ackbij2lem3  9101  cfss  9125  fin23lem7  9176  fin23lem11  9177  enfin2i  9181  isf32lem8  9220  isf34lem4  9237  isf34lem7  9239  isf34lem6  9240  isfin1-3  9246  fin1a2lem13  9272  ttukeylem6  9374  uzssz  11745  elfzoelz  12509  ackbijnn  14604  incexclem  14612  smuval2  15251  smupvallem  15252  smueqlem  15259  ramub1lem1  15777  ramub1lem2  15778  restid2  16138  mress  16300  mrcuni  16328  mreexexlem4d  16354  mreexexd  16355  mreexexdOLD  16356  mreexdomd  16357  acsfn  16367  isdrs2  16986  ipodrsima  17212  isacs3lem  17213  acsfiindd  17224  lagsubg2  17702  cntzrcl  17806  sylow1lem2  18060  sylow1lem3  18061  sylow1lem4  18062  sylow2alem2  18079  sylow2a  18080  lsmpropd  18136  lssacs  19015  lssacsex  19192  lbsextlem2  19207  lbsextlem3  19208  lbsextlem4  19209  elocv  20060  ppttop  20859  epttop  20861  clsval2  20902  mretopd  20944  neiss2  20953  neiptopnei  20984  ordtbas  21044  subbascn  21106  discmp  21249  uncmp  21254  conncompconn  21283  1stcfb  21296  2ndcdisj  21307  restnlly  21333  nllyrest  21337  nllyidm  21340  cldllycmp  21346  1stckgenlem  21404  dfac14  21469  xkoccn  21470  txnlly  21488  txkgen  21503  xkopt  21506  xkoco2cn  21509  xkoinjcn  21538  tgqtop  21563  nrmhmph  21645  fbelss  21684  fbssfi  21688  infil  21714  alexsubALTlem3  21900  alexsubALTlem4  21901  ustssxp  22055  trust  22080  utopsnneiplem  22098  blssm  22270  blin2  22281  metustss  22403  metustfbas  22409  metust  22410  psmetutop  22419  restmetu  22422  icccmplem2  22673  cncfrss  22741  cncfrss2  22742  bndth  22804  lebnum  22810  ovolicc2  23336  vitalilem5  23426  i1fd  23493  dvbsss  23711  perfdvf  23712  plybss  23995  wilthlem2  24840  f1otrg  25796  uhgrss  26004  upgrss  26028  usgrss  26114  eupth2lems  27216  ubthlem1  27854  elpwdifcl  29484  elpwiuncl  29485  ssnnssfz  29677  indf1ofs  30216  esumval  30236  esumel  30237  gsumesum  30249  esumlub  30250  esumpcvgval  30268  esumcvg  30276  elsigass  30316  ispisys2  30344  sigapildsyslem  30352  sigapildsys  30353  ldgenpisyslem1  30354  ldgenpisys  30357  dynkin  30358  rossspw  30360  srossspw  30367  ddemeas  30427  br2base  30459  sxbrsigalem0  30461  dya2iocucvr  30474  sxbrsigalem2  30476  sxbrsiga  30480  oms0  30487  omssubadd  30490  carsguni  30498  elcarsgss  30499  carsggect  30508  omsmeas  30513  eulerpartlemgvv  30566  coinfliplem  30668  ballotlemfmpn  30684  cvmliftmolem2  31390  cvmlift3lem8  31434  neibastop1  32479  neibastop2lem  32480  neibastop2  32481  filnetlem4  32501  cnambfre  33588  heiborlem3  33742  heiborlem5  33744  heiborlem6  33745  heiborlem10  33749  heibor  33750  mapd1o  37254  elrfi  37574  elrfirn  37575  elrfirn2  37576  ismrcd1  37578  istopclsd  37580  mrefg3  37588  aomclem2  37942  lsmfgcl  37961  lmhmfgima  37971  elmnc  38023  rfovcnvf1od  38615  rfovcnvfvd  38618  fsovrfovd  38620  fsovcnvlem  38624  dssmapnvod  38631  ntrk0kbimka  38654  clsk3nimkb  38655  neik0pk1imk0  38662  ntrclsfveq1  38675  ntrclsfveq2  38676  ntrclsfveq  38677  ntrclsss  38678  ntrclsiso  38682  ntrclsk2  38683  ntrclskb  38684  ntrclsk3  38685  ntrclsk13  38686  ntrclsk4  38687  ntrneifv3  38697  ntrneineine0lem  38698  ntrneineine1lem  38699  ntrneifv4  38700  ntrneiel2  38701  ntrneicls00  38704  ntrneicls11  38705  ntrneiiso  38706  ntrneik2  38707  ntrneikb  38709  ntrneixb  38710  ntrneik3  38711  ntrneix3  38712  ntrneik13  38713  ntrneix13  38714  ntrneik4w  38715  clsneiel2  38724  clsneifv3  38725  clsneifv4  38726  neicvgel2  38735  neicvgfv  38736  gneispb  38746  elpwinss  39530  stoweidlem39  40574  stoweidlem50  40585  sge0resrnlem  40938  sge0iunmptlemre  40950  psmeasurelem  41005  psmeasure  41006  ssnn0ssfz  42452
  Copyright terms: Public domain W3C validator