Theorem fveq1d 5557

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

Syntax hints:   → wi 4   = wceq 1364  ‘cfv 5255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263

This theorem is referenced by:  fveq12d  5562  funssfv  5581  fv2prc  5592  csbfv2g  5594  fvco4  5630  fvmptd  5639  fvmpt2d  5645  mpteqb  5649  fvmptt  5650  fnmptfvd  5663  fmptco  5725  fvunsng  5753  fvsng  5755  fsnunfv  5760  f1ocnvfv1  5821  f1ocnvfv2  5822  fcof1  5827  fcofo  5828  ofvalg  6142  offval2  6148  ofrfval2  6149  caofinvl  6157  tfrlemi1  6387  rdg0g  6443  freceq1  6447  oav  6509  omv  6510  oeiv  6511  pw2f1odclem  6892  mapxpen  6906  xpmapenlem  6907  nninfisollemne  7192  nninfisol  7194  exmidomni  7203  nninfwlpoimlemginf  7237  cc3  7330  fseq1p1m1  10163  seqeq3  10526  seq3f1olemqsum  10587  seq3f1olemstep  10588  seq3f1olemp  10589  seqf1oglem2  10594  seqf1og  10595  seq3id  10599  seq3z  10602  exp3val  10615  bcval5  10837  bcn2  10838  seq3coll  10916  shftcan1  10981  shftcan2  10982  shftvalg  10983  shftval4g  10984  climshft2  11452  sumeq2  11505  summodc  11529  zsumdc  11530  fsum3  11533  isumz  11535  fisumss  11538  fsum3cvg2  11540  isumsplit  11637  prodeq2w  11702  prodeq2  11703  prodmodc  11724  zproddc  11725  fprodseq  11729  prod1dc  11732  fprodssdc  11736  nninfctlemfo  12180  odzval  12382  1arithlem2  12505  fvsetsid  12655  setsslid  12672  setsslnid  12673  prdsex  12883  imasival  12892  imasbas  12893  imasplusg  12894  imasmulr  12895  igsumvalx  12975  gsumfzval  12977  gsumpropd  12978  gsumress  12981  gsumval2  12983  grpinvval  13118  grpsubfvalg  13120  grpsubpropdg  13179  grpsubpropd2  13180  mulgfvalg  13194  mulgpropdg  13237  submmulg  13239  subgmulg  13261  releqgg  13293  eqgex  13294  eqgfval  13295  gsumfzmptfidmadd  13412  unitinvcl  13622  unitinvinv  13623  unitlinv  13625  unitrinv  13626  unitnegcl  13629  dvrfvald  13632  dvrvald  13633  rdivmuldivd  13643  subrgugrp  13739  lspval  13889  ixpsnbasval  13965  lidlnegcl  13984  rspcl  13990  rspssid  13991  rspssp  13993  rspsn  14033  zrhmulg  14119  znzrhval  14146  ntrval  14289  clsval  14290  neival  14322  cnpval  14377  txmetcnp  14697  metcnpd  14699  limccl  14838  ellimc3apf  14839  cnplimclemr  14848  limccnp2cntop  14856  dvfvalap  14860  dvfre  14889  plyrecj  14941  lgsval4  15177  lgsmod  15183  peano4nninf  15566