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

Theorem fvmptd 6182
Description: Deduction version of fvmpt 6176. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
fvmptd.1 (𝜑𝐹 = (𝑥𝐷𝐵))
fvmptd.2 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
fvmptd.3 (𝜑𝐴𝐷)
fvmptd.4 (𝜑𝐶𝑉)
Assertion
Ref Expression
fvmptd (𝜑 → (𝐹𝐴) = 𝐶)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷   𝜑,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmptd
StepHypRef Expression
1 fvmptd.1 . . 3 (𝜑𝐹 = (𝑥𝐷𝐵))
21fveq1d 6090 . 2 (𝜑 → (𝐹𝐴) = ((𝑥𝐷𝐵)‘𝐴))
3 fvmptd.3 . . 3 (𝜑𝐴𝐷)
4 fvmptd.2 . . . . 5 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
53, 4csbied 3525 . . . 4 (𝜑𝐴 / 𝑥𝐵 = 𝐶)
6 fvmptd.4 . . . 4 (𝜑𝐶𝑉)
75, 6eqeltrd 2687 . . 3 (𝜑𝐴 / 𝑥𝐵𝑉)
8 eqid 2609 . . . 4 (𝑥𝐷𝐵) = (𝑥𝐷𝐵)
98fvmpts 6179 . . 3 ((𝐴𝐷𝐴 / 𝑥𝐵𝑉) → ((𝑥𝐷𝐵)‘𝐴) = 𝐴 / 𝑥𝐵)
103, 7, 9syl2anc 690 . 2 (𝜑 → ((𝑥𝐷𝐵)‘𝐴) = 𝐴 / 𝑥𝐵)
112, 10, 53eqtrd 2647 1 (𝜑 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  csb 3498  cmpt 4637  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-iota 5754  df-fun 5792  df-fv 5798
This theorem is referenced by:  fvmptdv2  6191  fvmptopab1  6572  bropfvvvv  7121  mpt2curryvald  7260  ttukeylem3  9193  ccatval1  13160  ccatval2  13161  repswsymb  13318  relexp1g  13560  rtrclreclem2  13593  rtrclreclem4  13595  dfrtrcl2  13596  lcmfval  15118  lcmf0val  15119  prmoval  15521  fvprmselelfz  15532  fvprmselgcd1  15533  prmodvdslcmf  15535  prmgap  15547  prmgaplcm  15548  prmgapprmo  15550  prdsvscafval  15909  mrcval  16039  cidval  16107  isofval  16186  isofn  16204  cicfval  16226  subcid  16276  idfu2nd  16306  resf2nd  16324  fuccoval  16392  fucid  16400  initoval  16416  termoval  16417  zerooval  16418  homaval  16450  idaval  16477  setcval  16496  setcid  16505  catcval  16515  catcid  16522  estrcval  16533  estrcid  16543  funcestrcsetclem1  16549  funcsetcestrclem1  16563  prf1  16609  prf2  16611  curf1  16634  curf11  16635  curf2val  16639  hofval  16661  hof2  16666  yonval  16670  yonedalem4a  16684  frmdval  17157  vrmdval  17163  pmtrdifwrdellem3  17672  gexval  17762  pj1val  17877  dpjval  18224  sraval  18943  opsrval  19241  cply1mul  19431  cply1coe0  19436  cply1coe0bi  19437  gsummoncoe1  19441  evls1sca  19455  frlmphl  19881  mat1rhmval  20046  scmatrhmval  20094  mvmulfv  20111  mavmulfv  20113  mdetuni0  20188  mat2pmatval  20290  m2cpm  20307  cpm2mval  20316  m2cpminvid2lem  20320  decpmatid  20336  decpmatmullem  20337  pmatcollpw2lem  20343  monmatcollpw  20345  pmatcollpw3fi1lem1  20352  pm2mpfval  20362  mply1topmatval  20370  mp2pm2mplem1  20372  mp2pm2mplem4  20375  pm2mpmhmlem2  20385  chpmatval  20397  chfacfscmul0  20424  chfacfscmulgsum  20426  chfacfpmmul0  20428  chfacfpmmulgsum  20430  lmfval  20788  kgenval  21090  ptval  21125  fcfval  21589  cnextfval  21618  ustval  21758  utopval  21788  ustuqtoplem  21795  utopsnneiplem  21803  tusval  21822  blfvalps  21939  tmsval  22037  metuval  22105  caufval  22799  rrxmvallem  22912  rrxmval  22913  taylpval  23842  efgh  24008  lgamgulmlem2  24473  lgamcvglem  24483  logexprlim  24667  dchrval  24676  dchr1  24699  gausslemma2dlem2  24809  gausslemma2dlem3  24810  gausslemma2dlem4  24811  2lgslem1b  24834  ishlg  25215  mirval  25268  mirfv  25269  israg  25310  perpln1  25323  perpln2  25324  isperp  25325  ishpg  25369  midf  25386  ismidb  25388  lmif  25395  islmib  25397  edgval  25634  wlkiswwlk2lem2  25986  clwlkisclwwlklem2fv1  26076  clwlkisclwwlklem2fv2  26077  sgnsval  28865  psgnfzto1stlem  28987  fzto1stfv1  28988  madjusmdetlem2  29028  metidval  29067  pstmval  29072  qqhvval  29161  indv  29208  indval  29209  indfval  29212  esummulc1  29276  esumcvg  29281  ofcval  29294  sigagenval  29336  measinb  29417  omsval  29488  omsfval  29489  omssubadd  29495  carsgval  29498  sitgfval  29536  eulerpartlemsv1  29551  eulerpartlems  29555  eulerpartlemgvv  29571  fibp1  29596  totprobd  29621  probmeasb  29625  cndprobval  29628  dstrvprob  29666  dstfrvinc  29671  dstfrvclim1  29672  ballotlemfval  29684  ballotlemsv  29704  gsumnunsn  29748  signsply0  29760  signstfval  29773  afsval  29808  cvmliftlem9  30335  mvrsval  30462  mrsubfval  30465  mrsubval  30466  msubfval  30481  msubval  30482  msrval  30495  fwddifval  31245  fwddifnval  31246  knoppcnlem1  31459  knoppcnlem4  31462  knoppcnlem6  31464  knoppcnlem7  31465  knoppcnlem9  31467  unbdqndv2lem2  31477  knoppndvlem4  31482  knoppndvlem6  31484  bj-finsumval0  32120  poimirlem1  32376  poimirlem2  32377  poimirlem5  32380  poimirlem6  32381  poimirlem7  32382  poimirlem10  32385  poimirlem11  32386  poimirlem12  32387  poimirlem19  32394  poimirlem22  32397  mblfinlem2  32413  areacirc  32471  cdleme31fv2  34495  tendopl2  34879  tendoi2  34897  erngplus2  34906  erngplus2-rN  34914  hlhilset  36040  itgpowd  36615  iunrelexpmin1  36815  iunrelexpmin2  36819  rfovfvd  37112  rfovfvfvd  37113  rfovcnvf1od  37114  rfovcnvfvd  37117  fsovfvd  37120  fsovfvfvd  37121  fsovcnvlem  37123  dssmapfvd  37127  dssmapfv2d  37128  dssmapfv3d  37129  dssmapnvod  37130  clsk3nimkb  37154  dvgrat  37329  radcnvrat  37331  hashnzfzclim  37339  binomcxplemnn0  37366  binomcxplemrat  37367  binomcxplemfrat  37368  binomcxplemradcnv  37369  binomcxplemcvg  37371  binomcxplemdvsum  37372  binomcxplemnotnn0  37373  projf1o  38177  mapss2  38188  fmuldfeqlem1  38446  clim1fr1  38465  climrec  38467  climexp  38469  climneg  38474  mullimcf  38487  divcnvg  38491  sumnnodd  38494  expfac  38521  fnlimfv  38527  fnlimabslt  38543  cncfshift  38556  icccncfext  38570  cncfioobdlem  38579  fprodsubrecnncnvlem  38591  fprodaddrecnncnvlem  38593  dvsinax  38598  fperdvper  38605  dvcosax  38613  ioodvbdlimc1lem1  38618  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  dvnmul  38630  dvnprodlem1  38633  dvnprodlem2  38634  dvnprodlem3  38635  itgsinexp  38643  itgcoscmulx  38658  itgsincmulx  38663  itgsubsticclem  38664  itgsubsticc  38665  itgiccshift  38669  stoweidlem7  38697  stoweidlem17  38707  stoweidlem32  38722  stoweidlem34  38724  wallispilem4  38758  wallispilem5  38759  wallispi  38760  wallispi2lem1  38761  wallispi2lem2  38762  wallispi2  38763  stirlinglem1  38764  stirlinglem2  38765  stirlinglem3  38766  stirlinglem4  38767  stirlinglem5  38768  stirlinglem7  38770  stirlinglem8  38771  stirlinglem10  38773  stirlinglem11  38774  stirlinglem12  38775  stirlinglem13  38776  stirlinglem14  38777  stirlinglem15  38778  dirkerval2  38784  dirkercncflem2  38794  fourierdlem7  38804  fourierdlem13  38810  fourierdlem14  38811  fourierdlem16  38813  fourierdlem18  38815  fourierdlem19  38816  fourierdlem21  38818  fourierdlem22  38819  fourierdlem26  38823  fourierdlem37  38834  fourierdlem39  38836  fourierdlem41  38838  fourierdlem48  38844  fourierdlem49  38845  fourierdlem50  38846  fourierdlem51  38847  fourierdlem53  38849  fourierdlem62  38858  fourierdlem63  38859  fourierdlem65  38861  fourierdlem73  38869  fourierdlem74  38870  fourierdlem75  38871  fourierdlem76  38872  fourierdlem79  38875  fourierdlem81  38877  fourierdlem82  38878  fourierdlem83  38879  fourierdlem84  38880  fourierdlem88  38884  fourierdlem89  38885  fourierdlem90  38886  fourierdlem91  38887  fourierdlem92  38888  fourierdlem93  38889  fourierdlem97  38893  fourierdlem101  38897  fourierdlem103  38899  fourierdlem104  38900  fourierdlem111  38907  fourierdlem112  38908  fouriersw  38921  elaa2lem  38923  etransclem1  38925  etransclem12  38936  etransclem13  38937  etransclem17  38941  etransclem18  38942  etransclem21  38945  etransclem27  38951  etransclem31  38955  etransclem32  38956  etransclem33  38957  etransclem35  38959  etransclem46  38970  etransclem48  38972  rrxtopnfi  38979  salgenval  39014  sge0val  39056  sge0z  39065  sge0snmpt  39073  sge0xp  39119  nnfoctbdjlem  39145  psmeasurelem  39160  psmeasure  39161  meaiuninclem  39170  meaiininclem  39173  omeiunltfirp  39206  carageniuncllem1  39208  carageniuncllem2  39209  caratheodorylem1  39213  0ome  39216  vonval  39227  ovnval  39228  ovnval2  39232  hoicvr  39235  ovnval2b  39239  hoiprodcl2  39242  ovnlecvr  39245  ovncvrrp  39251  ovn0lem  39252  ovnsubaddlem1  39257  hsphoif  39263  hoidmvval  39264  hsphoival  39266  hoidmv1le  39281  hoidmvlelem3  39284  ovnhoilem1  39288  ovnhoilem2  39289  hoidifhspval  39295  hspval  39296  ovncvr2  39298  hoidifhspval2  39302  hoidifhspval3  39306  hspmbllem2  39314  ovnsubadd2lem  39332  vonioolem2  39369  vonicclem2  39372  issmflem  39410  smfid  39436  iccpval  39751  fmtno  39777  prmdvdsfmtnof1  39835  mptmpt2opabbrd  40155  edgaval  40348  uvtxaval  40608  vtxdgfval  40678  1wlksfval  40806  wlksfval  40807  crctcsh1wlkn0lem2  41009  crctcsh1wlkn0lem3  41010  crctcsh  41022  wwlks  41033  1wlkiswwlks2lem2  41062  1wlkpwwlkf1ouspgr  41071  clwwlks  41182  clwlkclwwlklem2fv1  41199  clwlkclwwlklem2fv2  41200  2wspmdisj  41496  fusgreghash2wsp  41497  av-numclwlk1lem2fv  41518  av-numclwlk2lem2fv  41529  clintopval  41625  assintopval  41626  c0mgm  41694  c0mhm  41695  c0snmgmhm  41699  c0snmhm  41700  zrrnghm  41702  rngcvalALTV  41748  rngcval  41749  rngcidALTV  41778  zrinitorngc  41787  zrtermorngc  41788  ringcvalALTV  41794  ringcval  41795  funcringcsetcALTV2lem1  41823  ringcidALTV  41841  funcringcsetclem1ALTV  41846  zrtermoringc  41857  rhmsubcALTVlem3  41894  scmsuppss  41942  ply1mulgsum  41967  lincop  41986  lincext3  42034  lindslinindsimp1  42035  lindsrng01  42046  lincresunit2  42056  lincresunit3lem1  42057  islindeps2  42061  fdivmptfv  42132  refdivmptfv  42133  bigoval  42136  blenval  42158  digfval  42184  amgmwlem  42313
  Copyright terms: Public domain W3C validator