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

Theorem fvmptd 6778
Description: Deduction version of fvmpt 6771. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) (Proof shortened by AV, 29-Mar-2024.)
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 . 2 (𝜑𝐹 = (𝑥𝐷𝐵))
2 fvmptd.2 . 2 ((𝜑𝑥 = 𝐴) → 𝐵 = 𝐶)
3 fvmptd.3 . 2 (𝜑𝐴𝐷)
4 fvmptd.4 . 2 (𝜑𝐶𝑉)
5 nfv 1914 . 2 𝑥𝜑
6 nfcv 2980 . 2 𝑥𝐴
7 nfcv 2980 . 2 𝑥𝐶
81, 2, 3, 4, 5, 6, 7fvmptdf 6777 1 (𝜑 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398   = wceq 1536  wcel 2113  cmpt 5149  cfv 6358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-iota 6317  df-fun 6360  df-fv 6366
This theorem is referenced by:  fvmptd2  6779  fvmptdv2  6789  fsplitfpar  7817  mpocurryvald  7939  ttukeylem3  9936  ccatval1  13933  ccatval1OLD  13934  ccatval2  13935  repswsymb  14139  relexp1g  14388  rtrclreclem2  14421  rtrclreclem4  14423  dfrtrcl2  14424  prmodvdslcmf  16386  prmgap  16398  prmgaplcm  16399  prmgapprmo  16401  prdsvscafval  16756  mrcval  16884  cidval  16951  subcid  17120  idfu2nd  17150  resf2nd  17168  fuccoval  17236  fucid  17244  homaval  17294  idaval  17321  setcid  17349  catcid  17366  estrcid  17387  funcestrcsetclem1  17393  funcsetcestrclem1  17407  prf1  17453  prf2  17455  curf1  17478  curf11  17479  curf2val  17483  hof2  17510  yonedalem4a  17528  vrmdval  18025  smndex1gbas  18070  smndex1gid  18071  smndex1n0mnd  18080  mulgnngsum  18236  pj1val  18824  dpjval  19181  sraval  19951  opsrval  20258  selvfval  20333  selvval  20334  mhpval  20336  cply1mul  20465  cply1coe0  20470  cply1coe0bi  20471  gsummoncoe1  20475  evls1sca  20489  frlmphl  20928  mvmulfv  21156  mavmulfv  21158  mdetuni0  21233  mat2pmatval  21335  m2cpm  21352  cpm2mval  21361  m2cpminvid2lem  21365  decpmatid  21381  decpmatmullem  21382  pmatcollpw2lem  21388  monmatcollpw  21390  pm2mpfval  21407  mp2pm2mplem4  21420  pm2mpmhmlem2  21430  chpmatval  21442  fcfval  22644  cnextfval  22673  utopsnneiplem  22859  rrxmvallem  24010  rrxmval  24011  taylpval  24958  lgamgulmlem2  25610  lgamcvglem  25620  logexprlim  25804  dchr1  25836  ishlg  26391  mirval  26444  mirfv  26445  ishpg  26548  lmif  26574  islmib  26576  lmodvslmhm  30692  psgnfzto1stlem  30746  tocycfv  30755  sgnsval  30807  madjusmdetlem2  31097  metidval  31134  pstmval  31139  qqhvval  31228  indval  31276  indfval  31279  esummulc1  31344  esumcvg  31349  ofcval  31362  sigagenval  31403  measinb  31484  omsfval  31556  omssubadd  31562  sitgfval  31603  eulerpartlemsv1  31618  eulerpartlems  31622  fibp1  31663  totprobd  31688  probmeasb  31692  dstrvprob  31733  dstfrvinc  31738  dstfrvclim1  31739  ballotlemfval  31751  ballotlemsv  31771  gsumnunsn  31815  signsply0  31825  signstfval  31838  fdvneggt  31875  fdvnegge  31877  itgexpif  31881  breprexplema  31905  vtsval  31912  logdivsqrle  31925  hgt750lemg  31929  afsval  31946  lpadval  31951  cvmliftlem9  32544  goel  32598  satf0suc  32627  sat1el2xp  32630  fmlafv  32631  fmla  32632  fmlasuc0  32635  ex-sategoelel  32672  ex-sategoelelomsuc  32677  mvrsval  32756  mrsubfval  32759  mrsubval  32760  msubfval  32775  msubval  32776  msrval  32789  fwddifval  33627  fwddifnval  33628  knoppcnlem1  33836  knoppcnlem4  33839  knoppcnlem6  33841  knoppcnlem7  33842  bj-imdirval2  34477  bj-fvmptunsn2  34544  bj-endval  34600  poimirlem1  34897  poimirlem2  34898  poimirlem5  34901  poimirlem6  34902  poimirlem7  34903  poimirlem10  34906  poimirlem11  34907  poimirlem12  34908  poimirlem19  34915  poimirlem22  34918  mblfinlem2  34934  areacirc  34991  tendopl2  37917  tendoi2  37935  erngplus2  37944  erngplus2-rN  37952  hlhilset  39074  itgpowd  39827  rfovfvd  40354  rfovfvfvd  40355  rfovcnvf1od  40356  rfovcnvfvd  40359  fsovfvd  40362  fsovfvfvd  40363  fsovcnvlem  40365  dssmapfv2d  40370  dssmapfv3d  40371  dssmapnvod  40372  clsk3nimkb  40396  dvgrat  40650  radcnvrat  40652  hashnzfzclim  40660  binomcxplemnn0  40687  binomcxplemrat  40688  binomcxplemfrat  40689  binomcxplemradcnv  40690  binomcxplemcvg  40692  binomcxplemdvsum  40693  binomcxplemnotnn0  40694  mapss2  41474  fmuldfeqlem1  41869  clim1fr1  41888  climrec  41890  climexp  41892  climneg  41897  divcnvg  41914  sumnnodd  41917  supcnvlimsup  42027  icccncfext  42176  cncfioobdlem  42185  fprodsubrecnncnvlem  42197  fprodaddrecnncnvlem  42199  dvsinax  42203  fperdvper  42209  dvcosax  42217  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  dvnmul  42234  dvnprodlem1  42237  dvnprodlem2  42238  dvnprodlem3  42239  itgsinexp  42246  itgcoscmulx  42260  itgsincmulx  42265  itgsubsticclem  42266  itgsubsticc  42267  itgiccshift  42271  wallispilem5  42361  wallispi  42362  wallispi2lem1  42363  wallispi2lem2  42364  wallispi2  42365  stirlinglem1  42366  stirlinglem2  42367  stirlinglem3  42368  stirlinglem4  42369  stirlinglem5  42370  stirlinglem7  42372  stirlinglem8  42373  stirlinglem10  42375  stirlinglem11  42376  stirlinglem12  42377  stirlinglem13  42378  stirlinglem14  42379  stirlinglem15  42380  dirkerval2  42386  dirkercncflem2  42396  fourierdlem7  42406  fourierdlem13  42412  fourierdlem14  42413  fourierdlem16  42415  fourierdlem18  42417  fourierdlem19  42418  fourierdlem21  42420  fourierdlem22  42421  fourierdlem26  42425  fourierdlem37  42436  fourierdlem39  42438  fourierdlem41  42440  fourierdlem48  42446  fourierdlem49  42447  fourierdlem50  42448  fourierdlem51  42449  fourierdlem53  42451  fourierdlem62  42460  fourierdlem63  42461  fourierdlem65  42463  fourierdlem73  42471  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem79  42477  fourierdlem81  42479  fourierdlem82  42480  fourierdlem83  42481  fourierdlem84  42482  fourierdlem88  42486  fourierdlem89  42487  fourierdlem90  42488  fourierdlem91  42489  fourierdlem92  42490  fourierdlem93  42491  fourierdlem97  42495  fourierdlem101  42499  fourierdlem103  42501  fourierdlem104  42502  fourierdlem111  42509  fourierdlem112  42510  fouriersw  42523  elaa2lem  42525  etransclem13  42539  etransclem17  42543  etransclem18  42544  etransclem21  42547  etransclem31  42557  etransclem32  42558  etransclem33  42559  etransclem35  42561  etransclem46  42572  etransclem48  42574  rrxtopnfi  42579  salgenval  42613  sge0val  42655  sge0z  42664  sge0snmpt  42672  sge0xp  42718  nnfoctbdjlem  42744  omeiunltfirp  42808  caratheodorylem1  42815  0ome  42818  ovnval2  42834  hoicvr  42837  ovncvrrp  42853  ovn0lem  42854  ovnsubaddlem1  42859  hsphoif  42865  hsphoival  42868  hoidmv1le  42883  hoidmvlelem3  42886  ovnhoilem2  42891  ovncvr2  42900  hoidifhspval2  42904  hoidifhspval3  42908  hspmbllem2  42916  smfid  43036  fvmptrab  43498  fundcmpsurinjlem3  43567  sprval  43648  prproropreud  43678  isomuspgrlem2a  44000  c0mgm  44187  c0mhm  44188  c0snmgmhm  44192  c0snmhm  44193  zrrnghm  44195  rngcvalALTV  44239  rngcidALTV  44269  zrinitorngc  44278  zrtermorngc  44279  ringcvalALTV  44285  funcringcsetcALTV2lem1  44314  ringcidALTV  44332  funcringcsetclem1ALTV  44337  zrtermoringc  44348  rhmsubcALTVlem3  44384  scmsuppss  44427  ply1mulgsum  44451  lindslinindsimp1  44519  lindsrng01  44530  islindeps2  44545  fdivmptfv  44612  refdivmptfv  44613  amgmwlem  44910
  Copyright terms: Public domain W3C validator