Theorem fveq2d 5500

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

Syntax hints:   → wi 4   = wceq 1348  ‘cfv 5198

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206

This theorem is referenced by:  2fveq3  5501  fveq12d  5503  fveqeq2d  5504  csbfvg  5534  fvmptdf  5583  fvmptt  5587  fcof1  5762  oveq1  5860  oveq2  5861  fvoveq1d  5875  caofinvl  6083  op1stg  6129  op2ndg  6130  ot1stg  6131  ot2ndg  6132  eloprabi  6175  1stconst  6200  algrflemg  6209  tfrlem1  6287  tfrlem3ag  6288  tfrlem3a  6289  tfrlem9  6298  tfr0dm  6301  tfrlemisucaccv  6304  tfrlemiubacc  6309  tfrlemiex  6310  tfrlemi1  6311  tfr1onlem3ag  6316  tfr1onlemsucaccv  6320  tfr1onlemubacc  6325  tfr1onlemex  6326  tfr1onlemaccex  6327  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllemubacc  6338  tfrcllemex  6339  tfrcllemaccex  6340  tfrcllemres  6341  tfrcldm  6342  rdgivallem  6360  rdgival  6361  rdgss  6362  rdgisuc1  6363  rdgon  6365  rdg0  6366  frec0g  6376  frecabcl  6378  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecsuc  6386  frecrdg  6387  oav2  6442  omv2  6444  xpdom2  6809  xpmapenlem  6827  xpmapen  6828  ac6sfi  6876  1stinl  7051  2ndinl  7052  1stinr  7053  2ndinr  7054  updjudhcoinlf  7057  updjudhcoinrg  7058  caseinl  7068  caseinr  7069  omp1eomlem  7071  omp1eom  7072  difinfsn  7077  ctmlemr  7085  ctm  7086  ctssdclemn0  7087  ctssdccl  7088  nnnninfeq  7104  nnnninfeq2  7105  enomnilem  7114  enmkvlem  7137  enwomnilem  7145  exmidfodomrlemeldju  7176  exmidfodomrlemreseldju  7177  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  cc2  7229  cc3  7230  ltdfpr  7468  genpelvl  7474  genpelvu  7475  recexpr  7600  cauappcvgprlem1  7621  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemcl  7638  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem1  7641  caucvgprlem2  7642  caucvgpr  7644  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemnkeqj  7652  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemloc  7665  caucvgprprlemclphr  7667  caucvgprprlemexbt  7668  caucvgprprlem1  7671  caucvgprprlem2  7672  caucvgsr  7764  axcaucvglemval  7859  axcaucvglemres  7861  fv0p1e1  8993  uzin  9519  cnref1o  9609  fzsuc2  10035  fseq1m1p1  10051  fzoss2  10128  elfzonlteqm1  10166  divfl0  10252  flqzadd  10254  fldiv4p1lem1div2  10261  ceilqval  10262  flqdiv  10277  modqval  10280  modqfrac  10293  modqmulnn  10298  modqid  10305  modqcyc  10315  modqdi  10348  frec2uzuzd  10358  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgtcl  10368  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  frecuzrdgfunlem  10375  frecuzrdgsuctlem  10379  iseqovex  10412  iseqvalcbv  10413  seq3val  10414  seqvalcd  10415  seq3m1  10424  seq3shft2  10429  monoord  10432  monoord2  10433  iseqf1olemqval  10443  iseqf1olemab  10445  iseqf1olemqk  10450  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  iseqf1olemfvp  10453  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3f1olemp  10458  seq3f1oleml  10459  seq3homo  10466  exp3val  10478  expnegap0  10484  facnn2  10668  facwordi  10674  faclbnd6  10678  bcval  10683  bccmpl  10688  bcn0  10689  bcm1k  10694  bcp1n  10695  bcn2  10698  hashinfom  10712  hashennn  10714  hashsng  10733  omgadd  10737  hashprg  10743  fihashssdif  10753  hashdifpr  10755  hashfzo  10757  hashfzp1  10759  hashxp  10761  zfz1isolemiso  10774  zfz1iso  10776  shftval2  10790  shftval3  10791  shftval4  10792  shftval5  10793  seq3shft  10802  imval  10814  imre  10815  reim  10816  crim  10822  reim0  10825  mulreap  10828  recj  10831  reneg  10832  readd  10833  resub  10834  remullem  10835  redivap  10838  imcj  10839  imneg  10840  imadd  10841  imsub  10842  imdivap  10845  cjsub  10856  cjexp  10857  cjreim2  10868  cjap  10870  cjdivap  10873  cnrecnv  10874  cvg1nlemcau  10948  cvg1nlemres  10949  absval  10965  rennim  10966  sqrtdiv  11006  sqrtmsq  11009  absneg  11014  abscj  11016  absval2  11021  absreim  11032  absmul  11033  absdivap  11034  absid  11035  absre  11041  absexp  11043  absexpzap  11044  absimle  11048  abssub  11065  abs3dif  11069  abs2dif  11070  abs2dif2  11071  recan  11073  cau3lem  11078  max0addsup  11183  minabs  11199  bdtrilem  11202  clim  11244  clim2  11246  clim0  11248  clim0c  11249  climi0  11252  climconst  11253  climshftlemg  11265  climcn1  11271  climcn2  11272  addcn2  11273  subcn2  11274  mulcn2  11275  reccn2ap  11276  cjcn2  11279  recn2  11280  imcn2  11281  iser3shft  11309  climcau  11310  climcvg1nlem  11312  climcvg1n  11313  serf0  11315  summodclem3  11343  summodclem2a  11344  summodc  11346  fsumf1o  11353  sumsnf  11372  fsumm1  11379  fsumcnv  11400  fsumabs  11428  fsumrelem  11434  iserabs  11438  hash2iun1dif1  11443  isumshft  11453  isumsplit  11454  expcnvap0  11465  expcnv  11467  cvgratnnlemseq  11489  cvgratnnlemrate  11493  cvgratz  11495  mertenslemub  11497  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodmodclem3  11538  fprodf1o  11551  prodsnf  11555  fprodm1  11561  fprodabs  11579  fprodcnv  11588  efcllemp  11621  efcj  11636  efaddlem  11637  efcan  11639  efsub  11644  efexp  11645  efzval  11646  efgt0  11647  eftlub  11653  efltim  11661  sinval  11665  cosval  11666  tanval3ap  11677  resinval  11678  recosval  11679  resin4p  11681  recos4p  11682  sinneg  11689  cosneg  11690  efmival  11696  efeul  11697  sinadd  11699  cosadd  11700  sinsub  11703  cossub  11704  addsin  11705  subsin  11706  addcos  11709  subcos  11710  sincossq  11711  sin2t  11712  cos2t  11713  sin01bnd  11720  cos01bnd  11721  sin02gt0  11726  cos12dec  11730  absefi  11731  absef  11732  absefib  11733  efieq1re  11734  demoivre  11735  demoivreALT  11736  flodddiv4  11893  alginv  12001  algcvg  12002  eucalgval  12008  eucalginv  12010  eucalglt  12011  eucalgcvga  12012  eucalg  12013  lcmgcd  12032  lcm1  12035  sqpweven  12129  2sqpwodd  12130  sqne2sq  12131  qnumval  12139  qdenval  12140  qden1elz  12159  nn0sqrtelqelz  12160  phival  12167  dfphi2  12174  phiprmpw  12176  phiprm  12177  eulerthlemth  12186  hashgcdeq  12193  phisum  12194  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem12  12229  pythagtriplem14  12231  fldivp1  12300  ennnfonelemg  12358  ennnfonelemp1  12361  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemnn0  12377  ctinfomlemom  12382  ctiunctlemu1st  12389  ctiunctlemu2nd  12390  ctiunctlemudc  12392  ctiunctlemfo  12394  isstruct2im  12426  isstruct2r  12427  strslfv3  12461  setsslid  12466  ressid2  12477  ressval2  12478  ismhm  12685  mhmpropd  12689  mhmlin  12690  mhmf1o  12693  mhmco  12705  istps  12824  tpspropd  12828  eltpsg  12832  txvalex  13048  txval  13049  txbasval  13061  upxp  13066  uptx  13068  txrest  13070  cnmpt11  13077  cnmpt21  13085  hmeontr  13107  txhmeo  13113  psmetxrge0  13126  xmetunirn  13152  mopnval  13236  mopntopon  13237  isxms  13245  isxms2  13246  isms  13247  msrtri  13270  xmspropd  13271  mspropd  13272  setsmsbasg  13273  setsmsdsg  13274  setsmstsetg  13275  comet  13293  metcnpi  13309  metcnpi2  13310  cnbl0  13328  cnblcld  13329  resubmet  13342  elcncf  13354  cncfi  13359  rescncf  13362  mulc1cncf  13370  cncfco  13372  cncfmptid  13377  addccncf  13380  cdivcncfap  13381  negcncf  13382  mulcncflem  13384  ivthinclemlopn  13408  ivthinclemuopn  13410  limccl  13422  ellimc3apf  13423  limcimolemlt  13427  cnplimclemle  13431  limccnpcntop  13438  reldvg  13442  dvfvalap  13444  dveflem  13481  dvef  13482  sin0pilem1  13496  ef2kpi  13521  sinperlem  13523  sin2kpi  13526  cos2kpi  13527  sin2pim  13528  cos2pim  13529  ptolemy  13539  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  sinq12gt0  13545  tangtx  13553  sincosq1eq  13554  abssinper  13561  sinkpi  13562  coskpi  13563  cosq34lt1  13565  relogeftb  13580  relogoprlem  13583  relogexp  13587  rpcxpef  13609  logcxp  13612  1cxp  13615  ecxp  13616  rpcxpadd  13620  rpmulcxp  13624  cxpmul  13627  abscxp  13629  logsqrt  13637  rpabscxpbnd  13653  rpcxplogb  13676  lgsval  13699  lgsval2lem  13705  lgsval4a  13717  lgsdi  13732  nnsf  14038  peano4nninf  14039  peano3nninf  14040  nninfalllem1  14041  nninfall  14042  nninfsellemdc  14043  nninfsellemeq  14047  nninfsellemqall  14048  nninfsellemeqinf  14049  nninfsel  14050  exmidsbthr  14055  qdencn  14059  refeq  14060  isomninnlem  14062  apdifflemr  14079  apdiff  14080  ismkvnnlem  14084  nconstwlpolem  14096