Theorem fveq1d 5700

Description: Equality deduction for function value. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
fveq1d.1	⊢ (𝜑 → 𝐹 = 𝐺)

Assertion

Ref	Expression
fveq1d	⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))

Proof of Theorem fveq1d

Step	Hyp	Ref	Expression
1		fveq1d.1	. 2 ⊢ (𝜑 → 𝐹 = 𝐺)
2		fveq1 5697	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))

This proof depends on syntax axioms:   → wi 4   = wceq 1402  ‘cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388

This theorem is used by:  fveq12d  5705  funssfv  5724  fv2prc  5738  csbfv2g  5740  fvco4  5780  fvmptd  5789  fvmpt2d  5795  mpteqb  5799  fvmptt  5800  fnmptfvd  5816  fmptco  5877  fvunsng  5912  fvsng  5914  fsnunfv  5919  f1ocnvfv1  5986  f1ocnvfv2  5987  fcof1  5992  fcofo  5993  ofvalg  6316  offval2  6322  ofrfval2  6323  caofinvl  6332  tfrlemi1  6608  rdg0g  6664  freceq1  6668  oav  6732  omv  6733  oeiv  6734  pw2f1odclem  7140  mapxpen  7154  xpmapenlem  7155  2omap  7324  nninfisollemne  7477  nninfisol  7479  exmidomni  7488  nninfwlpoimlemginf  7522  cc3  7640  indval0  9306  fseq1p1m1  10517  seqeq3  10909  seq3f1olemqsum  10970  seq3f1olemstep  10971  seq3f1olemp  10972  seqf1oglem2  10977  seqf1og  10978  seq3id  10982  seq3z  10985  exp3val  10998  bcval5  11222  bcn2  11223  hashf1lem1  11306  seq3coll  11315  s1fv  11415  ccat1st1st  11430  ccat2s1fvwd  11436  swrdfv  11446  pfxfv  11477  swrdswrd  11498  shftcan1  11620  shftcan2  11621  shftvalg  11622  shftval4g  11623  climshft2  12096  sumeq2  12149  summodc  12174  zsumdc  12175  fsum3  12178  isumz  12180  fisumss  12183  fsum3cvg2  12185  isumsplit  12282  prodeq2w  12347  prodeq2  12348  prodmodc  12369  zproddc  12370  fprodseq  12374  prod1dc  12377  fprodssdc  12381  nninfctlemfo  12841  odzval  13048  1arithlem2  13171  ballotfileme  13293  ballotfilemi  13300  ballotfi  13339  fvsetsid  13443  setsslid  13460  setsslnid  13461  imasival  13685  imasbas  13686  imasplusg  13687  imasmulr  13688  gzsumvalx  13767  gzsumfzval  13769  gzsumress  13770  gzsumval2  13772  grpinvval  13906  grpsubfvalg  13908  grpsubpropdg  13967  grpsubpropd2  13968  mulgfvalg  13982  mulgpropdg  14025  submmulg  14027  subgmulg  14049  releqgg  14081  eqgex  14082  eqgfval  14083  gzsumshift  14238  prdsex  14278  prdsval  14279  prdsplusgfval  14290  prdsmulrfval  14292  pwsinvg  14321  unitinvcl  14538  unitinvinv  14539  unitlinv  14541  unitrinv  14542  unitnegcl  14545  dvrfvald  14548  dvrvald  14549  rdivmuldivd  14559  subrgugrp  14656  rrgsupp  14682  opprdrng  14728  lspval  14835  ixpsnbasval  14911  lidlnegcl  14930  rspcl  14936  rspssid  14937  rspssp  14939  rspsn  14979  zrhmulg  15063  znzrhval  15090  aspval  15123  psrdifi  15211  psrdirfi  15212  mvrval  15215  mvrval2  15216  mvrf1fi  15219  mplsubgfilemcl  15232  mplsubgfileminv  15233  mplnegfi  15238  ntrval  15353  clsval  15354  neival  15386  cnpval  15441  txmetcnp  15761  metcnpd  15763  limccl  15902  ellimc3apf  15903  cnplimclemr  15912  limccnp2cntop  15920  dvfvalap  15924  dvfre  15953  plycoeid3  16000  plyrecj  16006  lgsval4  16361  lgsmod  16367  uhgrspansubgrlem  16739  vtxdgfval  16751  vtxdgfifival  16754  vtxdgop  16755  vtxdeqd  16759  vtxdfifiun  16760  1loopgrvd0fi  16769  1hevtxdg0fi  16770  1hevtxdg1en  16771  1hegrvtxdg1fi  16772  wksfval  16785  wlkres  16842  eupth2fi  16942  pw1map  17247  peano4nninf  17272