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

Theorem fvmptd 6767
Description: Deduction version of fvmpt 6761. (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 6665 . 2 (𝜑 → (𝐹𝐴) = ((𝑥𝐷𝐵)‘𝐴))
3 fvmptd.3 . . 3 (𝜑𝐴𝐷)
4 fvmptd.2 . . . . 5 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
53, 4csbied 3916 . . . 4 (𝜑𝐴 / 𝑥𝐵 = 𝐶)
6 fvmptd.4 . . . 4 (𝜑𝐶𝑉)
75, 6eqeltrd 2910 . . 3 (𝜑𝐴 / 𝑥𝐵𝑉)
8 eqid 2818 . . . 4 (𝑥𝐷𝐵) = (𝑥𝐷𝐵)
98fvmpts 6764 . . 3 ((𝐴𝐷𝐴 / 𝑥𝐵𝑉) → ((𝑥𝐷𝐵)‘𝐴) = 𝐴 / 𝑥𝐵)
103, 7, 9syl2anc 584 . 2 (𝜑 → ((𝑥𝐷𝐵)‘𝐴) = 𝐴 / 𝑥𝐵)
112, 10, 53eqtrd 2857 1 (𝜑 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  csb 3880  cmpt 5137  cfv 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356
This theorem is referenced by:  fvmptd2  6768  fvmptdv2  6778  fsplitfpar  7803  mpocurryvald  7925  ttukeylem3  9921  ccatval1  13918  ccatval1OLD  13919  ccatval2  13920  repswsymb  14124  relexp1g  14373  rtrclreclem2  14406  rtrclreclem4  14408  dfrtrcl2  14409  prmodvdslcmf  16371  prmgap  16383  prmgaplcm  16384  prmgapprmo  16386  prdsvscafval  16741  mrcval  16869  cidval  16936  subcid  17105  idfu2nd  17135  resf2nd  17153  fuccoval  17221  fucid  17229  homaval  17279  idaval  17306  setcid  17334  catcid  17351  estrcid  17372  funcestrcsetclem1  17378  funcsetcestrclem1  17392  prf1  17438  prf2  17440  curf1  17463  curf11  17464  curf2val  17468  hof2  17495  yonedalem4a  17513  vrmdval  18010  mulgnngsum  18171  pj1val  18750  dpjval  19107  sraval  19877  opsrval  20183  selvfval  20258  selvval  20259  mhpval  20261  cply1mul  20390  cply1coe0  20395  cply1coe0bi  20396  gsummoncoe1  20400  evls1sca  20414  frlmphl  20853  mvmulfv  21081  mavmulfv  21083  mdetuni0  21158  mat2pmatval  21260  m2cpm  21277  cpm2mval  21286  m2cpminvid2lem  21290  decpmatid  21306  decpmatmullem  21307  pmatcollpw2lem  21313  monmatcollpw  21315  pm2mpfval  21332  mp2pm2mplem4  21345  pm2mpmhmlem2  21355  chpmatval  21367  fcfval  22569  cnextfval  22598  utopsnneiplem  22783  rrxmvallem  23934  rrxmval  23935  taylpval  24882  lgamgulmlem2  25534  lgamcvglem  25544  logexprlim  25728  dchr1  25760  ishlg  26315  mirval  26368  mirfv  26369  ishpg  26472  lmif  26498  islmib  26500  lmodvslmhm  30615  psgnfzto1stlem  30669  tocycfv  30678  sgnsval  30730  madjusmdetlem2  30992  metidval  31029  pstmval  31034  qqhvval  31123  indval  31171  indfval  31174  esummulc1  31239  esumcvg  31244  ofcval  31257  sigagenval  31298  measinb  31379  omsfval  31451  omssubadd  31457  sitgfval  31498  eulerpartlemsv1  31513  eulerpartlems  31517  fibp1  31558  totprobd  31583  probmeasb  31587  dstrvprob  31628  dstfrvinc  31633  dstfrvclim1  31634  ballotlemfval  31646  ballotlemsv  31666  gsumnunsn  31710  signsply0  31720  signstfval  31733  fdvneggt  31770  fdvnegge  31772  itgexpif  31776  breprexplema  31800  vtsval  31807  logdivsqrle  31820  hgt750lemg  31824  afsval  31841  lpadval  31846  cvmliftlem9  32437  goel  32491  satf0suc  32520  sat1el2xp  32523  fmlafv  32524  fmla  32525  fmlasuc0  32528  ex-sategoelel  32565  ex-sategoelelomsuc  32570  mvrsval  32649  mrsubfval  32652  mrsubval  32653  msubfval  32668  msubval  32669  msrval  32682  fwddifval  33520  fwddifnval  33521  knoppcnlem1  33729  knoppcnlem4  33732  knoppcnlem6  33734  knoppcnlem7  33735  bj-imdirval2  34365  bj-fvmptunsn2  34432  poimirlem1  34774  poimirlem2  34775  poimirlem5  34778  poimirlem6  34779  poimirlem7  34780  poimirlem10  34783  poimirlem11  34784  poimirlem12  34785  poimirlem19  34792  poimirlem22  34795  mblfinlem2  34811  areacirc  34868  tendopl2  37793  tendoi2  37811  erngplus2  37820  erngplus2-rN  37828  hlhilset  38950  itgpowd  39699  rfovfvd  40226  rfovfvfvd  40227  rfovcnvf1od  40228  rfovcnvfvd  40231  fsovfvd  40234  fsovfvfvd  40235  fsovcnvlem  40237  dssmapfv2d  40242  dssmapfv3d  40243  dssmapnvod  40244  clsk3nimkb  40268  dvgrat  40521  radcnvrat  40523  hashnzfzclim  40531  binomcxplemnn0  40558  binomcxplemrat  40559  binomcxplemfrat  40560  binomcxplemradcnv  40561  binomcxplemcvg  40563  binomcxplemdvsum  40564  binomcxplemnotnn0  40565  mapss2  41344  fmuldfeqlem1  41739  clim1fr1  41758  climrec  41760  climexp  41762  climneg  41767  divcnvg  41784  sumnnodd  41787  supcnvlimsup  41897  icccncfext  42046  cncfioobdlem  42055  fprodsubrecnncnvlem  42067  fprodaddrecnncnvlem  42069  dvsinax  42073  fperdvper  42079  dvcosax  42087  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  dvnmul  42104  dvnprodlem1  42107  dvnprodlem2  42108  dvnprodlem3  42109  itgsinexp  42116  itgcoscmulx  42130  itgsincmulx  42135  itgsubsticclem  42136  itgsubsticc  42137  itgiccshift  42141  wallispilem5  42231  wallispi  42232  wallispi2lem1  42233  wallispi2lem2  42234  wallispi2  42235  stirlinglem1  42236  stirlinglem2  42237  stirlinglem3  42238  stirlinglem4  42239  stirlinglem5  42240  stirlinglem7  42242  stirlinglem8  42243  stirlinglem10  42245  stirlinglem11  42246  stirlinglem12  42247  stirlinglem13  42248  stirlinglem14  42249  stirlinglem15  42250  dirkerval2  42256  dirkercncflem2  42266  fourierdlem7  42276  fourierdlem13  42282  fourierdlem14  42283  fourierdlem16  42285  fourierdlem18  42287  fourierdlem19  42288  fourierdlem21  42290  fourierdlem22  42291  fourierdlem26  42295  fourierdlem37  42306  fourierdlem39  42308  fourierdlem41  42310  fourierdlem48  42316  fourierdlem49  42317  fourierdlem50  42318  fourierdlem51  42319  fourierdlem53  42321  fourierdlem62  42330  fourierdlem63  42331  fourierdlem65  42333  fourierdlem73  42341  fourierdlem74  42342  fourierdlem75  42343  fourierdlem76  42344  fourierdlem79  42347  fourierdlem81  42349  fourierdlem82  42350  fourierdlem83  42351  fourierdlem84  42352  fourierdlem88  42356  fourierdlem89  42357  fourierdlem90  42358  fourierdlem91  42359  fourierdlem92  42360  fourierdlem93  42361  fourierdlem97  42365  fourierdlem101  42369  fourierdlem103  42371  fourierdlem104  42372  fourierdlem111  42379  fourierdlem112  42380  fouriersw  42393  elaa2lem  42395  etransclem13  42409  etransclem17  42413  etransclem18  42414  etransclem21  42417  etransclem31  42427  etransclem32  42428  etransclem33  42429  etransclem35  42431  etransclem46  42442  etransclem48  42444  rrxtopnfi  42449  salgenval  42483  sge0val  42525  sge0z  42534  sge0snmpt  42542  sge0xp  42588  nnfoctbdjlem  42614  omeiunltfirp  42678  caratheodorylem1  42685  0ome  42688  ovnval2  42704  hoicvr  42707  ovncvrrp  42723  ovn0lem  42724  ovnsubaddlem1  42729  hsphoif  42735  hsphoival  42738  hoidmv1le  42753  hoidmvlelem3  42756  ovnhoilem2  42761  ovncvr2  42770  hoidifhspval2  42774  hoidifhspval3  42778  hspmbllem2  42786  smfid  42906  fvmptrab  43368  fundcmpsurinjlem3  43437  sprval  43518  prproropreud  43548  isomuspgrlem2a  43870  smndex1gbas  44002  smndex1gid  44003  smndex1n0mnd  44012  c0mgm  44108  c0mhm  44109  c0snmgmhm  44113  c0snmhm  44114  zrrnghm  44116  rngcvalALTV  44160  rngcidALTV  44190  zrinitorngc  44199  zrtermorngc  44200  ringcvalALTV  44206  funcringcsetcALTV2lem1  44235  ringcidALTV  44253  funcringcsetclem1ALTV  44258  zrtermoringc  44269  rhmsubcALTVlem3  44305  scmsuppss  44348  ply1mulgsum  44372  lindslinindsimp1  44440  lindsrng01  44451  islindeps2  44466  fdivmptfv  44533  refdivmptfv  44534  amgmwlem  44831
  Copyright terms: Public domain W3C validator