Theorem fveq2d 5344

Description: Equality deduction for function value. (Contributed by NM, 29-May-1999.)

Hypothesis

Ref	Expression
fveq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
fveq2d	⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))

Proof of Theorem fveq2d

Step	Hyp	Ref	Expression
1		fveq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		fveq2 5340	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐵))

Syntax hints:   → wi 4   = wceq 1296  ‘cfv 5049

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-rex 2376  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-br 3868  df-iota 5014  df-fv 5057

This theorem is referenced by:  2fveq3  5345  fveq12d  5347  fveqeq2d  5348  csbfvg  5377  fvmptdf  5426  fvmptt  5430  fcof1  5600  oveq1  5697  oveq2  5698  fvoveq1d  5712  caofinvl  5915  op1stg  5959  op2ndg  5960  ot1stg  5961  ot2ndg  5962  eloprabi  6004  1stconst  6024  algrflemg  6033  tfrlem1  6111  tfrlem3ag  6112  tfrlem3a  6113  tfrlem9  6122  tfr0dm  6125  tfrlemisucaccv  6128  tfrlemiubacc  6133  tfrlemiex  6134  tfrlemi1  6135  tfr1onlem3ag  6140  tfr1onlemsucaccv  6144  tfr1onlemubacc  6149  tfr1onlemex  6150  tfr1onlemaccex  6151  tfrcllemsucaccv  6157  tfrcllembxssdm  6159  tfrcllemubacc  6162  tfrcllemex  6163  tfrcllemaccex  6164  tfrcllemres  6165  tfrcldm  6166  rdgivallem  6184  rdgival  6185  rdgss  6186  rdgisuc1  6187  rdgon  6189  rdg0  6190  frec0g  6200  frecabcl  6202  freccllem  6205  frecfcllem  6207  frecsuclem  6209  frecsuc  6210  frecrdg  6211  oav2  6264  omv2  6266  xpdom2  6627  xpmapenlem  6645  xpmapen  6646  ac6sfi  6694  1stinl  6845  2ndinl  6846  1stinr  6847  2ndinr  6848  updjudhcoinlf  6851  updjudhcoinrg  6852  caseinl  6862  ctmlemr  6870  ctm  6871  enomnilem  6881  exmidfodomrlemeldju  6922  exmidfodomrlemreseldju  6923  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  ltdfpr  7162  genpelvl  7168  genpelvu  7169  recexpr  7294  cauappcvgprlem1  7315  caucvgprlemnkj  7322  caucvgprlemnbj  7323  caucvgprlemm  7324  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprlemcl  7332  caucvgprlemladdfu  7333  caucvgprlemladdrl  7334  caucvgprlem1  7335  caucvgprlem2  7336  caucvgpr  7338  caucvgprprlemell  7341  caucvgprprlemelu  7342  caucvgprprlemcbv  7343  caucvgprprlemval  7344  caucvgprprlemnkeqj  7346  caucvgprprlemmu  7351  caucvgprprlemopl  7353  caucvgprprlemlol  7354  caucvgprprlemopu  7355  caucvgprprlemloc  7359  caucvgprprlemclphr  7361  caucvgprprlemexbt  7362  caucvgprprlem1  7365  caucvgprprlem2  7366  caucvgsr  7444  axcaucvglemval  7529  axcaucvglemres  7531  fv0p1e1  8635  uzin  9150  cnref1o  9232  fzsuc2  9642  fseq1m1p1  9658  fzoss2  9732  elfzonlteqm1  9770  divfl0  9852  flqzadd  9854  fldiv4p1lem1div2  9861  ceilqval  9862  flqdiv  9877  modqval  9880  modqfrac  9893  modqmulnn  9898  modqid  9905  modqcyc  9915  modqdi  9948  frec2uzuzd  9958  frec2uzrdg  9965  frecuzrdgrcl  9966  frecuzrdgtcl  9968  frecuzrdgsuc  9970  frecuzrdgrclt  9971  frecuzrdgg  9972  frecuzrdgfunlem  9975  frecuzrdgsuctlem  9979  iseqovex  10016  iseqval  10017  iseqvalcbv  10018  iseqvalt  10019  seq3val  10020  iseqfclt  10025  iseqp1  10028  iseqp1t  10029  seq3m1  10033  seq3shft2  10038  monoord  10042  monoord2  10043  iseqf1olemqval  10053  iseqf1olemab  10055  iseqf1olemqk  10060  iseqf1olemjpcl  10061  iseqf1olemqpcl  10062  iseqf1olemfvp  10063  seq3f1olemqsumkj  10064  seq3f1olemqsumk  10065  seq3f1olemqsum  10066  seq3f1olemp  10068  seq3f1oleml  10069  seq3homo  10076  exp3val  10088  expnegap0  10094  facnn2  10273  facwordi  10279  faclbnd6  10283  bcval  10288  bccmpl  10293  bcn0  10294  bcm1k  10299  bcp1n  10300  bcn2  10303  hashinfom  10317  hashennn  10319  hashsng  10337  omgadd  10341  hashprg  10347  fihashssdif  10357  hashdifpr  10359  hashfzo  10361  hashfzp1  10363  hashxp  10365  zfz1isolemiso  10375  zfz1iso  10377  shftval2  10391  shftval3  10392  shftval4  10393  shftval5  10394  seq3shft  10403  imval  10415  imre  10416  reim  10417  crim  10423  reim0  10426  mulreap  10429  recj  10432  reneg  10433  readd  10434  resub  10435  remullem  10436  redivap  10439  imcj  10440  imneg  10441  imadd  10442  imsub  10443  imdivap  10446  cjsub  10457  cjexp  10458  cjreim2  10469  cjap  10471  cjdivap  10474  cnrecnv  10475  cvg1nlemcau  10548  cvg1nlemres  10549  absval  10565  rennim  10566  sqrtdiv  10606  sqrtmsq  10609  absneg  10614  abscj  10616  absval2  10621  absreim  10632  absmul  10633  absdivap  10634  absid  10635  absre  10641  absexp  10643  absexpzap  10644  absimle  10648  abssub  10665  abs3dif  10669  abs2dif  10670  abs2dif2  10671  recan  10673  cau3lem  10678  max0addsup  10783  minabs  10798  bdtrilem  10801  clim  10840  clim2  10842  clim0  10844  clim0c  10845  climi0  10848  climconst  10849  climshftlemg  10861  climcn1  10867  climcn2  10868  addcn2  10869  subcn2  10870  mulcn2  10871  reccn2ap  10872  cjcn2  10875  recn2  10876  imcn2  10877  iser3shft  10905  climcau  10906  climcvg1nlem  10908  climcvg1n  10909  serf0  10911  summodclem3  10939  summodclem2a  10940  summodc  10942  fsumf1o  10949  sumsnf  10968  fsumm1  10975  fsumcnv  10996  fsumabs  11024  fsumrelem  11030  iserabs  11034  hash2iun1dif1  11039  isumshft  11049  isumsplit  11050  expcnvap0  11061  expcnv  11063  cvgratnnlemseq  11085  cvgratnnlemrate  11089  cvgratz  11091  mertenslemub  11093  mertenslemi1  11094  mertenslem2  11095  mertensabs  11096  efcllemp  11113  efcj  11128  efaddlem  11129  efcan  11131  efsub  11136  efexp  11137  efzval  11138  efgt0  11139  eftlub  11145  efltim  11153  sinval  11158  cosval  11159  tanval3ap  11170  resinval  11171  recosval  11172  resin4p  11174  recos4p  11175  sinneg  11182  cosneg  11183  efmival  11189  efeul  11190  sinadd  11192  cosadd  11193  sinsub  11196  cossub  11197  addsin  11198  subsin  11199  addcos  11202  subcos  11203  sincossq  11204  sin2t  11205  cos2t  11206  sin01bnd  11213  cos01bnd  11214  sin02gt0  11219  absefi  11223  absef  11224  absefib  11225  efieq1re  11226  demoivre  11227  demoivreALT  11228  flodddiv4  11377  alginv  11472  algcvg  11473  eucalgval  11479  eucalginv  11481  eucalglt  11482  eucalgcvga  11483  eucalg  11484  lcmgcd  11503  lcm1  11506  sqpweven  11596  2sqpwodd  11597  sqne2sq  11598  qnumval  11606  qdenval  11607  qden1elz  11626  nn0sqrtelqelz  11627  phival  11632  dfphi2  11639  phiprmpw  11641  phiprm  11642  hashgcdeq  11647  isstruct2im  11669  isstruct2r  11670  strslfv3  11704  setsslid  11709  ressid2  11718  ressval2  11719  istps  11898  tpspropd  11902  eltpsg  11906  cnmpt11  12121  psmetxrge0  12134  xmetunirn  12160  mopnval  12244  mopntopon  12245  isxms  12253  isxms2  12254  isms  12255  msrtri  12278  xmspropd  12279  mspropd  12280  setsmsbasg  12281  setsmsdsg  12282  setsmstsetg  12283  comet  12301  metcnpi  12313  metcnpi2  12314  cnbl0  12327  cnblcld  12328  resubmet  12338  elcncf  12342  cncfi  12347  rescncf  12350  mulc1cncf  12358  cncfco  12360  cncfmptid  12363  addccncf  12365  cdivcncfap  12366  negcncf  12367  mulcncflem  12369  nnsf  12616  peano4nninf  12617  peano3nninf  12618  nninfalllemn  12619  nninfalllem1  12620  nninfall  12621  nninfsellemdc  12623  nninfsellemeq  12627  nninfsellemqall  12628  nninfsellemeqinf  12629  nninfsel  12630  nninfomni  12632  exmidsbthr  12634  qdencn  12636