Theorem fveq1d 5516

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

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

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 3810  df-br 4003  df-iota 5177  df-fv 5223

This theorem is referenced by:  fveq12d  5521  funssfv  5540  csbfv2g  5551  fvco4  5587  fvmptd  5596  fvmpt2d  5601  mpteqb  5605  fvmptt  5606  fnmptfvd  5619  fmptco  5681  fvunsng  5709  fvsng  5711  fsnunfv  5716  f1ocnvfv1  5775  f1ocnvfv2  5776  fcof1  5781  fcofo  5782  ofvalg  6089  offval2  6095  ofrfval2  6096  caofinvl  6102  tfrlemi1  6330  rdg0g  6386  freceq1  6390  oav  6452  omv  6453  oeiv  6454  mapxpen  6845  xpmapenlem  6846  nninfisollemne  7126  nninfisol  7128  exmidomni  7137  nninfwlpoimlemginf  7171  cc3  7264  fseq1p1m1  10089  seqeq3  10445  seq3f1olemqsum  10495  seq3f1olemstep  10496  seq3f1olemp  10497  seq3id  10503  seq3z  10506  exp3val  10517  bcval5  10736  bcn2  10737  seq3coll  10815  shftcan1  10836  shftcan2  10837  shftvalg  10838  shftval4g  10839  climshft2  11307  sumeq2  11360  summodc  11384  zsumdc  11385  fsum3  11388  isumz  11390  fisumss  11393  fsum3cvg2  11395  isumsplit  11492  prodeq2w  11557  prodeq2  11558  prodmodc  11579  zproddc  11580  fprodseq  11584  prod1dc  11587  fprodssdc  11591  odzval  12233  1arithlem2  12354  fvsetsid  12488  setsslid  12505  setsslnid  12506  grpinvval  12848  grpsubfvalg  12850  grpsubpropdg  12906  grpsubpropd2  12907  mulgfvalg  12917  mulgpropdg  12956  subgmulg  12979  releqgg  13011  eqgfval  13012  unitinvcl  13223  unitinvinv  13224  unitlinv  13226  unitrinv  13227  unitnegcl  13230  dvrfvald  13233  dvrvald  13234  rdivmuldivd  13244  subrgugrp  13299  ntrval  13481  clsval  13482  neival  13514  cnpval  13569  txmetcnp  13889  metcnpd  13891  limccl  13999  ellimc3apf  14000  cnplimclemr  14009  limccnp2cntop  14017  dvfvalap  14021  dvfre  14045  lgsval4  14292  lgsmod  14298  peano4nninf  14615