Theorem fveq2d 5425

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

Syntax hints:   → wi 4   = wceq 1331  ‘cfv 5123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131

This theorem is referenced by:  2fveq3  5426  fveq12d  5428  fveqeq2d  5429  csbfvg  5459  fvmptdf  5508  fvmptt  5512  fcof1  5684  oveq1  5781  oveq2  5782  fvoveq1d  5796  caofinvl  6004  op1stg  6048  op2ndg  6049  ot1stg  6050  ot2ndg  6051  eloprabi  6094  1stconst  6118  algrflemg  6127  tfrlem1  6205  tfrlem3ag  6206  tfrlem3a  6207  tfrlem9  6216  tfr0dm  6219  tfrlemisucaccv  6222  tfrlemiubacc  6227  tfrlemiex  6228  tfrlemi1  6229  tfr1onlem3ag  6234  tfr1onlemsucaccv  6238  tfr1onlemubacc  6243  tfr1onlemex  6244  tfr1onlemaccex  6245  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllemubacc  6256  tfrcllemex  6257  tfrcllemaccex  6258  tfrcllemres  6259  tfrcldm  6260  rdgivallem  6278  rdgival  6279  rdgss  6280  rdgisuc1  6281  rdgon  6283  rdg0  6284  frec0g  6294  frecabcl  6296  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  frecrdg  6305  oav2  6359  omv2  6361  xpdom2  6725  xpmapenlem  6743  xpmapen  6744  ac6sfi  6792  1stinl  6959  2ndinl  6960  1stinr  6961  2ndinr  6962  updjudhcoinlf  6965  updjudhcoinrg  6966  caseinl  6976  caseinr  6977  omp1eomlem  6979  omp1eom  6980  difinfsn  6985  ctmlemr  6993  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  enomnilem  7010  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  ltdfpr  7314  genpelvl  7320  genpelvu  7321  recexpr  7446  cauappcvgprlem1  7467  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemm  7476  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemcl  7484  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlem1  7487  caucvgprlem2  7488  caucvgpr  7490  caucvgprprlemell  7493  caucvgprprlemelu  7494  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemnkeqj  7498  caucvgprprlemmu  7503  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemopu  7507  caucvgprprlemloc  7511  caucvgprprlemclphr  7513  caucvgprprlemexbt  7514  caucvgprprlem1  7517  caucvgprprlem2  7518  caucvgsr  7610  axcaucvglemval  7705  axcaucvglemres  7707  fv0p1e1  8835  uzin  9358  cnref1o  9440  fzsuc2  9859  fseq1m1p1  9875  fzoss2  9949  elfzonlteqm1  9987  divfl0  10069  flqzadd  10071  fldiv4p1lem1div2  10078  ceilqval  10079  flqdiv  10094  modqval  10097  modqfrac  10110  modqmulnn  10115  modqid  10122  modqcyc  10132  modqdi  10165  frec2uzuzd  10175  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgtcl  10185  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgg  10189  frecuzrdgfunlem  10192  frecuzrdgsuctlem  10196  iseqovex  10229  iseqvalcbv  10230  seq3val  10231  seqvalcd  10232  seq3m1  10241  seq3shft2  10246  monoord  10249  monoord2  10250  iseqf1olemqval  10260  iseqf1olemab  10262  iseqf1olemqk  10267  iseqf1olemjpcl  10268  iseqf1olemqpcl  10269  iseqf1olemfvp  10270  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  seq3f1olemp  10275  seq3f1oleml  10276  seq3homo  10283  exp3val  10295  expnegap0  10301  facnn2  10480  facwordi  10486  faclbnd6  10490  bcval  10495  bccmpl  10500  bcn0  10501  bcm1k  10506  bcp1n  10507  bcn2  10510  hashinfom  10524  hashennn  10526  hashsng  10544  omgadd  10548  hashprg  10554  fihashssdif  10564  hashdifpr  10566  hashfzo  10568  hashfzp1  10570  hashxp  10572  zfz1isolemiso  10582  zfz1iso  10584  shftval2  10598  shftval3  10599  shftval4  10600  shftval5  10601  seq3shft  10610  imval  10622  imre  10623  reim  10624  crim  10630  reim0  10633  mulreap  10636  recj  10639  reneg  10640  readd  10641  resub  10642  remullem  10643  redivap  10646  imcj  10647  imneg  10648  imadd  10649  imsub  10650  imdivap  10653  cjsub  10664  cjexp  10665  cjreim2  10676  cjap  10678  cjdivap  10681  cnrecnv  10682  cvg1nlemcau  10756  cvg1nlemres  10757  absval  10773  rennim  10774  sqrtdiv  10814  sqrtmsq  10817  absneg  10822  abscj  10824  absval2  10829  absreim  10840  absmul  10841  absdivap  10842  absid  10843  absre  10849  absexp  10851  absexpzap  10852  absimle  10856  abssub  10873  abs3dif  10877  abs2dif  10878  abs2dif2  10879  recan  10881  cau3lem  10886  max0addsup  10991  minabs  11007  bdtrilem  11010  clim  11050  clim2  11052  clim0  11054  clim0c  11055  climi0  11058  climconst  11059  climshftlemg  11071  climcn1  11077  climcn2  11078  addcn2  11079  subcn2  11080  mulcn2  11081  reccn2ap  11082  cjcn2  11085  recn2  11086  imcn2  11087  iser3shft  11115  climcau  11116  climcvg1nlem  11118  climcvg1n  11119  serf0  11121  summodclem3  11149  summodclem2a  11150  summodc  11152  fsumf1o  11159  sumsnf  11178  fsumm1  11185  fsumcnv  11206  fsumabs  11234  fsumrelem  11240  iserabs  11244  hash2iun1dif1  11249  isumshft  11259  isumsplit  11260  expcnvap0  11271  expcnv  11273  cvgratnnlemseq  11295  cvgratnnlemrate  11299  cvgratz  11301  mertenslemub  11303  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  prodmodclem3  11344  efcllemp  11364  efcj  11379  efaddlem  11380  efcan  11382  efsub  11387  efexp  11388  efzval  11389  efgt0  11390  eftlub  11396  efltim  11404  sinval  11409  cosval  11410  tanval3ap  11421  resinval  11422  recosval  11423  resin4p  11425  recos4p  11426  sinneg  11433  cosneg  11434  efmival  11440  efeul  11441  sinadd  11443  cosadd  11444  sinsub  11447  cossub  11448  addsin  11449  subsin  11450  addcos  11453  subcos  11454  sincossq  11455  sin2t  11456  cos2t  11457  sin01bnd  11464  cos01bnd  11465  sin02gt0  11470  cos12dec  11474  absefi  11475  absef  11476  absefib  11477  efieq1re  11478  demoivre  11479  demoivreALT  11480  flodddiv4  11631  alginv  11728  algcvg  11729  eucalgval  11735  eucalginv  11737  eucalglt  11738  eucalgcvga  11739  eucalg  11740  lcmgcd  11759  lcm1  11762  sqpweven  11853  2sqpwodd  11854  sqne2sq  11855  qnumval  11863  qdenval  11864  qden1elz  11883  nn0sqrtelqelz  11884  phival  11889  dfphi2  11896  phiprmpw  11898  phiprm  11899  hashgcdeq  11904  ennnfonelemg  11916  ennnfonelemp1  11919  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemnn0  11935  ctinfomlemom  11940  ctiunctlemu1st  11947  ctiunctlemu2nd  11948  ctiunctlemudc  11950  ctiunctlemfo  11952  isstruct2im  11969  isstruct2r  11970  strslfv3  12004  setsslid  12009  ressid2  12018  ressval2  12019  istps  12199  tpspropd  12203  eltpsg  12207  txvalex  12423  txval  12424  txbasval  12436  upxp  12441  uptx  12443  txrest  12445  cnmpt11  12452  cnmpt21  12460  hmeontr  12482  txhmeo  12488  psmetxrge0  12501  xmetunirn  12527  mopnval  12611  mopntopon  12612  isxms  12620  isxms2  12621  isms  12622  msrtri  12645  xmspropd  12646  mspropd  12647  setsmsbasg  12648  setsmsdsg  12649  setsmstsetg  12650  comet  12668  metcnpi  12684  metcnpi2  12685  cnbl0  12703  cnblcld  12704  resubmet  12717  elcncf  12729  cncfi  12734  rescncf  12737  mulc1cncf  12745  cncfco  12747  cncfmptid  12752  addccncf  12755  cdivcncfap  12756  negcncf  12757  mulcncflem  12759  ivthinclemlopn  12783  ivthinclemuopn  12785  limccl  12797  ellimc3apf  12798  limcimolemlt  12802  cnplimclemle  12806  limccnpcntop  12813  reldvg  12817  dvfvalap  12819  dveflem  12855  dvef  12856  sin0pilem1  12862  ef2kpi  12887  sinperlem  12889  sin2kpi  12892  cos2kpi  12893  sin2pim  12894  cos2pim  12895  ptolemy  12905  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  sinq12gt0  12911  tangtx  12919  sincosq1eq  12920  abssinper  12927  sinkpi  12928  coskpi  12929  cosq34lt1  12931  nnsf  13199  peano4nninf  13200  peano3nninf  13201  nninfalllemn  13202  nninfalllem1  13203  nninfall  13204  nninfsellemdc  13206  nninfsellemeq  13210  nninfsellemqall  13211  nninfsellemeqinf  13212  nninfsel  13213  nninfomni  13215  exmidsbthr  13218  qdencn  13222  refeq  13223  isomninnlem  13225