Theorem fveq1d 5519

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

Syntax hints:   → wi 4   = wceq 1353  ‘cfv 5218

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226

This theorem is referenced by:  fveq12d  5524  funssfv  5543  csbfv2g  5554  fvco4  5590  fvmptd  5599  fvmpt2d  5604  mpteqb  5608  fvmptt  5609  fnmptfvd  5622  fmptco  5684  fvunsng  5712  fvsng  5714  fsnunfv  5719  f1ocnvfv1  5780  f1ocnvfv2  5781  fcof1  5786  fcofo  5787  ofvalg  6094  offval2  6100  ofrfval2  6101  caofinvl  6107  tfrlemi1  6335  rdg0g  6391  freceq1  6395  oav  6457  omv  6458  oeiv  6459  mapxpen  6850  xpmapenlem  6851  nninfisollemne  7131  nninfisol  7133  exmidomni  7142  nninfwlpoimlemginf  7176  cc3  7269  fseq1p1m1  10096  seqeq3  10452  seq3f1olemqsum  10502  seq3f1olemstep  10503  seq3f1olemp  10504  seq3id  10510  seq3z  10513  exp3val  10524  bcval5  10745  bcn2  10746  seq3coll  10824  shftcan1  10845  shftcan2  10846  shftvalg  10847  shftval4g  10848  climshft2  11316  sumeq2  11369  summodc  11393  zsumdc  11394  fsum3  11397  isumz  11399  fisumss  11402  fsum3cvg2  11404  isumsplit  11501  prodeq2w  11566  prodeq2  11567  prodmodc  11588  zproddc  11589  fprodseq  11593  prod1dc  11596  fprodssdc  11600  odzval  12243  1arithlem2  12364  fvsetsid  12498  setsslid  12515  setsslnid  12516  prdsex  12723  imasival  12732  imasbas  12733  imasplusg  12734  imasmulr  12735  grpinvval  12921  grpsubfvalg  12923  grpsubpropdg  12979  grpsubpropd2  12980  mulgfvalg  12990  mulgpropdg  13030  subgmulg  13053  releqgg  13085  eqgfval  13086  unitinvcl  13297  unitinvinv  13298  unitlinv  13300  unitrinv  13301  unitnegcl  13304  dvrfvald  13307  dvrvald  13308  rdivmuldivd  13318  subrgugrp  13366  ntrval  13649  clsval  13650  neival  13682  cnpval  13737  txmetcnp  14057  metcnpd  14059  limccl  14167  ellimc3apf  14168  cnplimclemr  14177  limccnp2cntop  14185  dvfvalap  14189  dvfre  14213  lgsval4  14460  lgsmod  14466  peano4nninf  14794