Theorem fveq2d 5559

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 5555	. 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-3an 982  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-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263

This theorem is referenced by:  2fveq3  5560  fveq12d  5562  fveqeq2d  5563  csbfvg  5595  fvmptdf  5646  fvmptt  5650  fcof1  5827  oveq1  5926  oveq2  5927  fvoveq1d  5941  caofinvl  6157  op1stg  6205  op2ndg  6206  ot1stg  6207  ot2ndg  6208  eloprabi  6251  1stconst  6276  algrflemg  6285  tfrlem1  6363  tfrlem3ag  6364  tfrlem3a  6365  tfrlem9  6374  tfr0dm  6377  tfrlemisucaccv  6380  tfrlemiubacc  6385  tfrlemiex  6386  tfrlemi1  6387  tfr1onlem3ag  6392  tfr1onlemsucaccv  6396  tfr1onlemubacc  6401  tfr1onlemex  6402  tfr1onlemaccex  6403  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllemubacc  6414  tfrcllemex  6415  tfrcllemaccex  6416  tfrcllemres  6417  tfrcldm  6418  rdgivallem  6436  rdgival  6437  rdgss  6438  rdgisuc1  6439  rdgon  6441  rdg0  6442  frec0g  6452  frecabcl  6454  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecsuc  6462  frecrdg  6463  oav2  6518  omv2  6520  xpdom2  6887  xpmapenlem  6907  xpmapen  6908  ac6sfi  6956  1stinl  7135  2ndinl  7136  1stinr  7137  2ndinr  7138  updjudhcoinlf  7141  updjudhcoinrg  7142  caseinl  7152  caseinr  7153  omp1eomlem  7155  omp1eom  7156  difinfsn  7161  ctmlemr  7169  ctm  7170  ctssdclemn0  7171  ctssdccl  7172  nninfninc  7184  nnnninfeq  7189  nnnninfeq2  7190  enomnilem  7199  enmkvlem  7222  enwomnilem  7230  exmidfodomrlemeldju  7261  exmidfodomrlemreseldju  7262  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  cc2  7329  cc3  7330  ltdfpr  7568  genpelvl  7574  genpelvu  7575  recexpr  7700  cauappcvgprlem1  7721  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgprlem2  7742  caucvgpr  7744  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemnkeqj  7752  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemloc  7765  caucvgprprlemclphr  7767  caucvgprprlemexbt  7768  caucvgprprlem1  7771  caucvgprprlem2  7772  caucvgsr  7864  axcaucvglemval  7959  axcaucvglemres  7961  fv0p1e1  9099  uzin  9628  cnref1o  9719  fzsuc2  10148  fseq1m1p1  10164  fzoss2  10242  elfzonlteqm1  10280  divfl0  10368  flqzadd  10370  fldiv4p1lem1div2  10377  ceilqval  10380  flqdiv  10395  modqval  10398  modqfrac  10411  modqmulnn  10416  modqid  10423  modqcyc  10433  modqdi  10466  frec2uzuzd  10476  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgtcl  10486  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  frecuzrdgfunlem  10493  frecuzrdgsuctlem  10497  iseqovex  10532  iseqvalcbv  10533  seq3val  10534  seqvalcd  10535  seq3m1  10547  seq3shft2  10555  seqshft2g  10556  monoord  10559  monoord2  10560  iseqf1olemqval  10574  iseqf1olemab  10576  iseqf1olemqk  10581  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  iseqf1olemfvp  10584  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seq3f1olemp  10589  seq3f1oleml  10590  seqf1oglem1  10593  seqf1oglem2  10594  seqf1og  10595  seq3homo  10601  seqhomog  10604  exp3val  10615  expnegap0  10621  facnn2  10808  facwordi  10814  faclbnd6  10818  bcval  10823  bccmpl  10828  bcn0  10829  bcm1k  10834  bcp1n  10835  bcn2  10838  hashinfom  10852  hashennn  10854  hashsng  10872  omgadd  10876  hashprg  10882  fihashssdif  10892  hashdifpr  10894  hashfzo  10896  hashfzp1  10898  hashxp  10900  zfz1isolemiso  10913  zfz1iso  10915  shftval2  10973  shftval3  10974  shftval4  10975  shftval5  10976  seq3shft  10985  imval  10997  imre  10998  reim  10999  crim  11005  reim0  11008  mulreap  11011  recj  11014  reneg  11015  readd  11016  resub  11017  remullem  11018  redivap  11021  imcj  11022  imneg  11023  imadd  11024  imsub  11025  imdivap  11028  cjsub  11039  cjexp  11040  cjreim2  11051  cjap  11053  cjdivap  11056  cnrecnv  11057  cvg1nlemcau  11131  cvg1nlemres  11132  absval  11148  rennim  11149  sqrtdiv  11189  sqrtmsq  11192  absneg  11197  abscj  11199  absval2  11204  absreim  11215  absmul  11216  absdivap  11217  absid  11218  absre  11224  absexp  11226  absexpzap  11227  absimle  11231  abssub  11248  abs3dif  11252  abs2dif  11253  abs2dif2  11254  recan  11256  cau3lem  11261  max0addsup  11366  minabs  11382  bdtrilem  11385  clim  11427  clim2  11429  clim0  11431  clim0c  11432  climi0  11435  climconst  11436  climshftlemg  11448  climcn1  11454  climcn2  11455  addcn2  11456  subcn2  11457  mulcn2  11458  reccn2ap  11459  cjcn2  11462  recn2  11463  imcn2  11464  iser3shft  11492  climcau  11493  climcvg1nlem  11495  climcvg1n  11496  serf0  11498  summodclem3  11526  summodclem2a  11527  summodc  11529  fsumf1o  11536  sumsnf  11555  fsumm1  11562  fsumcnv  11583  fsumabs  11611  fsumrelem  11617  iserabs  11621  hash2iun1dif1  11626  isumshft  11636  isumsplit  11637  expcnvap0  11648  expcnv  11650  cvgratnnlemseq  11672  cvgratnnlemrate  11676  cvgratz  11678  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  mertensabs  11683  prodmodclem3  11721  fprodf1o  11734  prodsnf  11738  fprodm1  11744  fprodabs  11762  fprodcnv  11771  efcllemp  11804  efcj  11819  efaddlem  11820  efcan  11822  efsub  11827  efexp  11828  efzval  11829  efgt0  11830  eftlub  11836  efltim  11844  sinval  11848  cosval  11849  tanval3ap  11860  resinval  11861  recosval  11862  resin4p  11864  recos4p  11865  sinneg  11872  cosneg  11873  efmival  11879  efeul  11880  sinadd  11882  cosadd  11883  sinsub  11886  cossub  11887  addsin  11888  subsin  11889  addcos  11892  subcos  11893  sincossq  11894  sin2t  11895  cos2t  11896  sin01bnd  11903  cos01bnd  11904  sin02gt0  11910  cos12dec  11914  absefi  11915  absef  11916  absefib  11917  efieq1re  11918  demoivre  11919  demoivreALT  11920  flodddiv4  12078  nninfctlemfo  12180  alginv  12188  algcvg  12189  eucalgval  12195  eucalginv  12197  eucalglt  12198  eucalgcvga  12199  eucalg  12200  lcmgcd  12219  lcm1  12222  sqpweven  12316  2sqpwodd  12317  sqne2sq  12318  qnumval  12326  qdenval  12327  qden1elz  12346  nn0sqrtelqelz  12347  phival  12354  dfphi2  12361  phiprmpw  12363  phiprm  12364  eulerthlemth  12373  hashgcdeq  12380  phisum  12381  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem12  12416  pythagtriplem14  12418  fldivp1  12489  4sqlem11  12542  ennnfonelemg  12563  ennnfonelemp1  12566  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemnn0  12582  ctinfomlemom  12587  ctiunctlemu1st  12594  ctiunctlemu2nd  12595  ctiunctlemudc  12597  ctiunctlemfo  12599  isstruct2im  12631  isstruct2r  12632  strslfv3  12667  setsslid  12672  ressbasd  12688  resseqnbasd  12694  ressplusgd  12749  ptex  12878  prdsex  12883  imasex  12891  imasival  12892  f1ocpbl  12897  f1ovscpbl  12898  imasaddvallemg  12901  qusval  12909  fvprif  12929  xpsff1o  12935  igsumvalx  12975  gsumprval  12985  ismhm  13036  mhmpropd  13041  mhmlin  13042  mhmf1o  13045  resmhm  13062  mhmco  13065  gsumwmhm  13073  grpinvsub  13157  imasgrp2  13183  imasgrp  13184  mhmlem  13187  mhmid  13188  mhmmnd  13189  ghmgrp  13191  mulgfvalg  13194  mulgval  13195  mulgnegnn  13205  mulgneg  13213  mulgnegneg  13214  mulgm1  13215  mulginvcom  13220  mulgz  13223  mulgnndir  13224  mulgdir  13227  mulgass  13232  mhmmulg  13236  subgmulg  13261  isnsg  13275  eqgfval  13295  ghmlin  13321  ghmid  13322  ghminv  13323  ghmsub  13324  ghmmulg  13329  resghm  13333  ghmeql  13340  ablsub2inv  13384  ghmcmn  13400  invghm  13402  imasabl  13409  gsumfzreidx  13410  gsumfzmhm  13416  mgpplusgg  13423  mgpbasg  13425  mgpscag  13426  mgptsetg  13427  mgpdsg  13429  rngm2neg  13448  imasrng  13455  isring  13499  ringm2neg  13554  imasring  13563  opprmulfvalg  13569  opprsllem  13573  isunitd  13605  opprunitd  13609  invrfvald  13621  rdivmuldivd  13643  rhmmul  13663  isrhm2d  13664  rhm1  13666  rhmdvdsr  13674  rhmopp  13675  rhmunitinv  13677  islmod  13790  islmodd  13792  scaffvalg  13805  lmodpropd  13848  lsssetm  13855  islssmd  13858  lssats2  13913  lspsnneg  13919  lspsnsub  13920  lspun0  13924  lmodindp1  13927  sralemg  13937  srascag  13941  sravscag  13942  sraipg  13943  rlmscabas  13959  ixpsnbasval  13965  2idlval  14001  2idlvalg  14002  mulgrhm2  14109  zlmlemg  14127  zlmsca  14131  zlmvscag  14132  znval  14135  znle  14136  znbaslemnn  14138  znidomb  14157  psrval  14163  psrbasg  14170  psrplusgg  14173  istps  14211  tpspropd  14215  eltpsg  14219  txvalex  14433  txval  14434  txbasval  14446  upxp  14451  uptx  14453  txrest  14455  cnmpt11  14462  cnmpt21  14470  hmeontr  14492  txhmeo  14498  psmetxrge0  14511  xmetunirn  14537  mopnval  14621  mopntopon  14622  isxms  14630  isxms2  14631  isms  14632  msrtri  14655  xmspropd  14656  mspropd  14657  setsmsbasg  14658  setsmsdsg  14659  setsmstsetg  14660  comet  14678  metcnpi  14694  metcnpi2  14695  cnbl0  14713  cnblcld  14714  resubmet  14735  mpomulcn  14745  elcncf  14752  cncfi  14757  rescncf  14760  mulc1cncf  14768  cncfco  14770  cncfmptid  14776  addccncf  14779  cdivcncfap  14783  negcncf  14784  mulcncflem  14786  ivthinclemlopn  14815  ivthinclemuopn  14817  limccl  14838  ellimc3apf  14839  limcimolemlt  14843  cnplimclemle  14847  limccnpcntop  14854  reldvg  14858  dvfvalap  14860  dveflem  14905  dvef  14906  plymullem1  14927  plycjlemc  14938  plycj  14939  plyrecj  14941  plyreres  14942  sin0pilem1  14957  ef2kpi  14982  sinperlem  14984  sin2kpi  14987  cos2kpi  14988  sin2pim  14989  cos2pim  14990  ptolemy  15000  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  sinq12gt0  15006  tangtx  15014  sincosq1eq  15015  abssinper  15022  sinkpi  15023  coskpi  15024  cosq34lt1  15026  relogeftb  15041  relogoprlem  15044  relogexp  15048  rpcxpef  15070  logcxp  15073  1cxp  15076  ecxp  15077  rpcxpadd  15081  rpmulcxp  15085  cxpmul  15088  abscxp  15090  logsqrt  15098  rpabscxpbnd  15114  rpcxplogb  15137  lgsval  15161  lgsval2lem  15167  lgsval4a  15179  lgsdi  15194  lgseisenlem3  15229  lgseisenlem4  15230  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  2lgslem1  15248  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  nnsf  15565  peano4nninf  15566  peano3nninf  15567  nninfalllem1  15568  nninfall  15569  nninfsellemdc  15570  nninfsellemeq  15574  nninfsellemqall  15575  nninfsellemeqinf  15576  nninfsel  15577  exmidsbthr  15583  qdencn  15587  refeq  15588  isomninnlem  15590  apdifflemr  15607  apdiff  15608  ismkvnnlem  15612  nconstwlpolem  15625