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

Theorem fvmptd 6768
Description: Deduction version of fvmpt 6762. (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 6666 . 2 (𝜑 → (𝐹𝐴) = ((𝑥𝐷𝐵)‘𝐴))
3 fvmptd.3 . . 3 (𝜑𝐴𝐷)
4 fvmptd.2 . . . . 5 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
53, 4csbied 3918 . . . 4 (𝜑𝐴 / 𝑥𝐵 = 𝐶)
6 fvmptd.4 . . . 4 (𝜑𝐶𝑉)
75, 6eqeltrd 2913 . . 3 (𝜑𝐴 / 𝑥𝐵𝑉)
8 eqid 2821 . . . 4 (𝑥𝐷𝐵) = (𝑥𝐷𝐵)
98fvmpts 6765 . . 3 ((𝐴𝐷𝐴 / 𝑥𝐵𝑉) → ((𝑥𝐷𝐵)‘𝐴) = 𝐴 / 𝑥𝐵)
103, 7, 9syl2anc 584 . 2 (𝜑 → ((𝑥𝐷𝐵)‘𝐴) = 𝐴 / 𝑥𝐵)
112, 10, 53eqtrd 2860 1 (𝜑 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  csb 3882  cmpt 5138  cfv 6349
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 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
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 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-iota 6308  df-fun 6351  df-fv 6357
This theorem is referenced by:  fvmptd2  6769  fvmptdv2  6779  fsplitfpar  7805  mpocurryvald  7927  ttukeylem3  9922  ccatval1  13920  ccatval1OLD  13921  ccatval2  13922  repswsymb  14126  relexp1g  14375  rtrclreclem2  14408  rtrclreclem4  14410  dfrtrcl2  14411  prmodvdslcmf  16373  prmgap  16385  prmgaplcm  16386  prmgapprmo  16388  prdsvscafval  16743  mrcval  16871  cidval  16938  subcid  17107  idfu2nd  17137  resf2nd  17155  fuccoval  17223  fucid  17231  homaval  17281  idaval  17308  setcid  17336  catcid  17353  estrcid  17374  funcestrcsetclem1  17380  funcsetcestrclem1  17394  prf1  17440  prf2  17442  curf1  17465  curf11  17466  curf2val  17470  hof2  17497  yonedalem4a  17515  vrmdval  18012  mulgnngsum  18173  pj1val  18752  dpjval  19109  sraval  19879  opsrval  20185  selvfval  20260  selvval  20261  mhpval  20263  cply1mul  20392  cply1coe0  20397  cply1coe0bi  20398  gsummoncoe1  20402  evls1sca  20416  frlmphl  20855  mvmulfv  21083  mavmulfv  21085  mdetuni0  21160  mat2pmatval  21262  m2cpm  21279  cpm2mval  21288  m2cpminvid2lem  21292  decpmatid  21308  decpmatmullem  21309  pmatcollpw2lem  21315  monmatcollpw  21317  pm2mpfval  21334  mp2pm2mplem4  21347  pm2mpmhmlem2  21357  chpmatval  21369  fcfval  22571  cnextfval  22600  utopsnneiplem  22785  rrxmvallem  23936  rrxmval  23937  taylpval  24884  lgamgulmlem2  25535  lgamcvglem  25545  logexprlim  25729  dchr1  25761  ishlg  26316  mirval  26369  mirfv  26370  ishpg  26473  lmif  26499  islmib  26501  lmodvslmhm  30616  psgnfzto1stlem  30670  tocycfv  30679  sgnsval  30731  madjusmdetlem2  30993  metidval  31030  pstmval  31035  qqhvval  31124  indval  31172  indfval  31175  esummulc1  31240  esumcvg  31245  ofcval  31258  sigagenval  31299  measinb  31380  omsfval  31452  omssubadd  31458  sitgfval  31499  eulerpartlemsv1  31514  eulerpartlems  31518  fibp1  31559  totprobd  31584  probmeasb  31588  dstrvprob  31629  dstfrvinc  31634  dstfrvclim1  31635  ballotlemfval  31647  ballotlemsv  31667  gsumnunsn  31711  signsply0  31721  signstfval  31734  fdvneggt  31771  fdvnegge  31773  itgexpif  31777  breprexplema  31801  vtsval  31808  logdivsqrle  31821  hgt750lemg  31825  afsval  31842  lpadval  31847  cvmliftlem9  32438  goel  32492  satf0suc  32521  sat1el2xp  32524  fmlafv  32525  fmla  32526  fmlasuc0  32529  ex-sategoelel  32566  ex-sategoelelomsuc  32571  mvrsval  32650  mrsubfval  32653  mrsubval  32654  msubfval  32669  msubval  32670  msrval  32683  fwddifval  33521  fwddifnval  33522  knoppcnlem1  33730  knoppcnlem4  33733  knoppcnlem6  33735  knoppcnlem7  33736  bj-imdirval2  34366  bj-fvmptunsn2  34433  poimirlem1  34775  poimirlem2  34776  poimirlem5  34779  poimirlem6  34780  poimirlem7  34781  poimirlem10  34784  poimirlem11  34785  poimirlem12  34786  poimirlem19  34793  poimirlem22  34796  mblfinlem2  34812  areacirc  34869  tendopl2  37795  tendoi2  37813  erngplus2  37822  erngplus2-rN  37830  hlhilset  38952  itgpowd  39701  rfovfvd  40228  rfovfvfvd  40229  rfovcnvf1od  40230  rfovcnvfvd  40233  fsovfvd  40236  fsovfvfvd  40237  fsovcnvlem  40239  dssmapfv2d  40244  dssmapfv3d  40245  dssmapnvod  40246  clsk3nimkb  40270  dvgrat  40524  radcnvrat  40526  hashnzfzclim  40534  binomcxplemnn0  40561  binomcxplemrat  40562  binomcxplemfrat  40563  binomcxplemradcnv  40564  binomcxplemcvg  40566  binomcxplemdvsum  40567  binomcxplemnotnn0  40568  mapss2  41348  fmuldfeqlem1  41743  clim1fr1  41762  climrec  41764  climexp  41766  climneg  41771  divcnvg  41788  sumnnodd  41791  supcnvlimsup  41901  icccncfext  42050  cncfioobdlem  42059  fprodsubrecnncnvlem  42071  fprodaddrecnncnvlem  42073  dvsinax  42077  fperdvper  42083  dvcosax  42091  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnmul  42108  dvnprodlem1  42111  dvnprodlem2  42112  dvnprodlem3  42113  itgsinexp  42120  itgcoscmulx  42134  itgsincmulx  42139  itgsubsticclem  42140  itgsubsticc  42141  itgiccshift  42145  wallispilem5  42235  wallispi  42236  wallispi2lem1  42237  wallispi2lem2  42238  wallispi2  42239  stirlinglem1  42240  stirlinglem2  42241  stirlinglem3  42242  stirlinglem4  42243  stirlinglem5  42244  stirlinglem7  42246  stirlinglem8  42247  stirlinglem10  42249  stirlinglem11  42250  stirlinglem12  42251  stirlinglem13  42252  stirlinglem14  42253  stirlinglem15  42254  dirkerval2  42260  dirkercncflem2  42270  fourierdlem7  42280  fourierdlem13  42286  fourierdlem14  42287  fourierdlem16  42289  fourierdlem18  42291  fourierdlem19  42292  fourierdlem21  42294  fourierdlem22  42295  fourierdlem26  42299  fourierdlem37  42310  fourierdlem39  42312  fourierdlem41  42314  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem51  42323  fourierdlem53  42325  fourierdlem62  42334  fourierdlem63  42335  fourierdlem65  42337  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem76  42348  fourierdlem79  42351  fourierdlem81  42353  fourierdlem82  42354  fourierdlem83  42355  fourierdlem84  42356  fourierdlem88  42360  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem92  42364  fourierdlem93  42365  fourierdlem97  42369  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  fourierdlem112  42384  fouriersw  42397  elaa2lem  42399  etransclem13  42413  etransclem17  42417  etransclem18  42418  etransclem21  42421  etransclem31  42431  etransclem32  42432  etransclem33  42433  etransclem35  42435  etransclem46  42446  etransclem48  42448  rrxtopnfi  42453  salgenval  42487  sge0val  42529  sge0z  42538  sge0snmpt  42546  sge0xp  42592  nnfoctbdjlem  42618  omeiunltfirp  42682  caratheodorylem1  42689  0ome  42692  ovnval2  42708  hoicvr  42711  ovncvrrp  42727  ovn0lem  42728  ovnsubaddlem1  42733  hsphoif  42739  hsphoival  42742  hoidmv1le  42757  hoidmvlelem3  42760  ovnhoilem2  42765  ovncvr2  42774  hoidifhspval2  42778  hoidifhspval3  42782  hspmbllem2  42790  smfid  42910  fvmptrab  43372  sprval  43488  prproropreud  43518  isomuspgrlem2a  43840  smndex1gbas  43972  smndex1gid  43973  smndex1n0mnd  43982  c0mgm  44078  c0mhm  44079  c0snmgmhm  44083  c0snmhm  44084  zrrnghm  44086  rngcvalALTV  44130  rngcidALTV  44160  zrinitorngc  44169  zrtermorngc  44170  ringcvalALTV  44176  funcringcsetcALTV2lem1  44205  ringcidALTV  44223  funcringcsetclem1ALTV  44228  zrtermoringc  44239  rhmsubcALTVlem3  44275  scmsuppss  44318  ply1mulgsum  44342  lindslinindsimp1  44410  lindsrng01  44421  islindeps2  44436  fdivmptfv  44503  refdivmptfv  44504  amgmwlem  44801
  Copyright terms: Public domain W3C validator