Theorem fveq1d 5697

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 5694	. 2 ⊢ (𝐹 = 𝐺 → (𝐹‘𝐴) = (𝐺‘𝐴))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐺‘𝐴))

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

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 4131  df-iota 5337  df-fv 5385

This theorem is used by:  fveq12d  5702  funssfv  5721  fv2prc  5735  csbfv2g  5737  fvco4  5777  fvmptd  5786  fvmpt2d  5792  mpteqb  5796  fvmptt  5797  fnmptfvd  5813  fmptco  5874  fvunsng  5909  fvsng  5911  fsnunfv  5916  f1ocnvfv1  5983  f1ocnvfv2  5984  fcof1  5989  fcofo  5990  ofvalg  6312  offval2  6318  ofrfval2  6319  caofinvl  6328  tfrlemi1  6603  rdg0g  6659  freceq1  6663  oav  6727  omv  6728  oeiv  6729  pw2f1odclem  7134  mapxpen  7148  xpmapenlem  7149  2omap  7318  nninfisollemne  7471  nninfisol  7473  exmidomni  7482  nninfwlpoimlemginf  7516  cc3  7634  indval0  9299  fseq1p1m1  10511  seqeq3  10902  seq3f1olemqsum  10963  seq3f1olemstep  10964  seq3f1olemp  10965  seqf1oglem2  10970  seqf1og  10971  seq3id  10975  seq3z  10978  exp3val  10991  bcval5  11215  bcn2  11216  hashf1lem1  11299  seq3coll  11308  s1fv  11408  ccat1st1st  11423  ccat2s1fvwd  11429  swrdfv  11439  pfxfv  11470  swrdswrd  11491  shftcan1  11613  shftcan2  11614  shftvalg  11615  shftval4g  11616  climshft2  12088  sumeq2  12141  summodc  12166  zsumdc  12167  fsum3  12170  isumz  12172  fisumss  12175  fsum3cvg2  12177  isumsplit  12274  prodeq2w  12339  prodeq2  12340  prodmodc  12361  zproddc  12362  fprodseq  12366  prod1dc  12369  fprodssdc  12373  nninfctlemfo  12833  odzval  13040  1arithlem2  13163  ballotfileme  13285  ballotfilemi  13292  ballotfi  13331  fvsetsid  13435  setsslid  13452  setsslnid  13453  imasival  13676  imasbas  13677  imasplusg  13678  imasmulr  13679  gzsumvalx  13758  gzsumfzval  13760  gzsumress  13761  gzsumval2  13763  grpinvval  13897  grpsubfvalg  13899  grpsubpropdg  13958  grpsubpropd2  13959  mulgfvalg  13973  mulgpropdg  14016  submmulg  14018  subgmulg  14040  releqgg  14072  eqgex  14073  eqgfval  14074  gzsumshift  14198  prdsex  14221  prdsval  14222  prdsplusgfval  14233  prdsmulrfval  14235  pwsinvg  14264  unitinvcl  14479  unitinvinv  14480  unitlinv  14482  unitrinv  14483  unitnegcl  14486  dvrfvald  14489  dvrvald  14490  rdivmuldivd  14500  subrgugrp  14597  rrgsupp  14623  opprdrng  14669  lspval  14776  ixpsnbasval  14852  lidlnegcl  14871  rspcl  14877  rspssid  14878  rspssp  14880  rspsn  14920  zrhmulg  15004  znzrhval  15031  aspval  15064  mplsubgfilemm  15138  mplsubgfilemcl  15139  mplsubgfileminv  15140  mplnegfi  15145  ntrval  15260  clsval  15261  neival  15293  cnpval  15348  txmetcnp  15668  metcnpd  15670  limccl  15809  ellimc3apf  15810  cnplimclemr  15819  limccnp2cntop  15827  dvfvalap  15831  dvfre  15860  plycoeid3  15907  plyrecj  15913  lgsval4  16237  lgsmod  16243  uhgrspansubgrlem  16615  vtxdgfval  16627  vtxdgfifival  16630  vtxdgop  16631  vtxdeqd  16635  vtxdfifiun  16636  1loopgrvd0fi  16645  1hevtxdg0fi  16646  1hevtxdg1en  16647  1hegrvtxdg1fi  16648  wksfval  16661  wlkres  16718  eupth2fi  16818  pw1map  17123  peano4nninf  17147