Theorem fveq2d 5521

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

Hypothesis

Ref	Expression
fveq2d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
fveq2d	|- ( ph -> ( F ` A ) = ( F ` B ) )

Proof of Theorem fveq2d

Step	Hyp	Ref	Expression
1		fveq2d.1	. 2 |- ( ph -> A = B )
2		fveq2 5517	. 2 |- ( A = B -> ( F ` A ) = ( F ` B ) )
3	1, 2	syl 14	1 |- ( ph -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1353   ` cfv 5218

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-3an 980  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-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226

This theorem is referenced by:  2fveq3  5522  fveq12d  5524  fveqeq2d  5525  csbfvg  5555  fvmptdf  5605  fvmptt  5609  fcof1  5786  oveq1  5884  oveq2  5885  fvoveq1d  5899  caofinvl  6107  op1stg  6153  op2ndg  6154  ot1stg  6155  ot2ndg  6156  eloprabi  6199  1stconst  6224  algrflemg  6233  tfrlem1  6311  tfrlem3ag  6312  tfrlem3a  6313  tfrlem9  6322  tfr0dm  6325  tfrlemisucaccv  6328  tfrlemiubacc  6333  tfrlemiex  6334  tfrlemi1  6335  tfr1onlem3ag  6340  tfr1onlemsucaccv  6344  tfr1onlemubacc  6349  tfr1onlemex  6350  tfr1onlemaccex  6351  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllemubacc  6362  tfrcllemex  6363  tfrcllemaccex  6364  tfrcllemres  6365  tfrcldm  6366  rdgivallem  6384  rdgival  6385  rdgss  6386  rdgisuc1  6387  rdgon  6389  rdg0  6390  frec0g  6400  frecabcl  6402  freccllem  6405  frecfcllem  6407  frecsuclem  6409  frecsuc  6410  frecrdg  6411  oav2  6466  omv2  6468  xpdom2  6833  xpmapenlem  6851  xpmapen  6852  ac6sfi  6900  1stinl  7075  2ndinl  7076  1stinr  7077  2ndinr  7078  updjudhcoinlf  7081  updjudhcoinrg  7082  caseinl  7092  caseinr  7093  omp1eomlem  7095  omp1eom  7096  difinfsn  7101  ctmlemr  7109  ctm  7110  ctssdclemn0  7111  ctssdccl  7112  nnnninfeq  7128  nnnninfeq2  7129  enomnilem  7138  enmkvlem  7161  enwomnilem  7169  exmidfodomrlemeldju  7200  exmidfodomrlemreseldju  7201  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidaclem  7209  cc2  7268  cc3  7269  ltdfpr  7507  genpelvl  7513  genpelvu  7514  recexpr  7639  cauappcvgprlem1  7660  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemm  7669  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemcl  7677  caucvgprlemladdfu  7678  caucvgprlemladdrl  7679  caucvgprlem1  7680  caucvgprlem2  7681  caucvgpr  7683  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemcbv  7688  caucvgprprlemval  7689  caucvgprprlemnkeqj  7691  caucvgprprlemmu  7696  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemopu  7700  caucvgprprlemloc  7704  caucvgprprlemclphr  7706  caucvgprprlemexbt  7707  caucvgprprlem1  7710  caucvgprprlem2  7711  caucvgsr  7803  axcaucvglemval  7898  axcaucvglemres  7900  fv0p1e1  9036  uzin  9562  cnref1o  9652  fzsuc2  10081  fseq1m1p1  10097  fzoss2  10174  elfzonlteqm1  10212  divfl0  10298  flqzadd  10300  fldiv4p1lem1div2  10307  ceilqval  10308  flqdiv  10323  modqval  10326  modqfrac  10339  modqmulnn  10344  modqid  10351  modqcyc  10361  modqdi  10394  frec2uzuzd  10404  frec2uzrdg  10411  frecuzrdgrcl  10412  frecuzrdgtcl  10414  frecuzrdgsuc  10416  frecuzrdgrclt  10417  frecuzrdgg  10418  frecuzrdgfunlem  10421  frecuzrdgsuctlem  10425  iseqovex  10458  iseqvalcbv  10459  seq3val  10460  seqvalcd  10461  seq3m1  10470  seq3shft2  10475  monoord  10478  monoord2  10479  iseqf1olemqval  10489  iseqf1olemab  10491  iseqf1olemqk  10496  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  iseqf1olemfvp  10499  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  seq3f1olemp  10504  seq3f1oleml  10505  seq3homo  10512  exp3val  10524  expnegap0  10530  facnn2  10716  facwordi  10722  faclbnd6  10726  bcval  10731  bccmpl  10736  bcn0  10737  bcm1k  10742  bcp1n  10743  bcn2  10746  hashinfom  10760  hashennn  10762  hashsng  10780  omgadd  10784  hashprg  10790  fihashssdif  10800  hashdifpr  10802  hashfzo  10804  hashfzp1  10806  hashxp  10808  zfz1isolemiso  10821  zfz1iso  10823  shftval2  10837  shftval3  10838  shftval4  10839  shftval5  10840  seq3shft  10849  imval  10861  imre  10862  reim  10863  crim  10869  reim0  10872  mulreap  10875  recj  10878  reneg  10879  readd  10880  resub  10881  remullem  10882  redivap  10885  imcj  10886  imneg  10887  imadd  10888  imsub  10889  imdivap  10892  cjsub  10903  cjexp  10904  cjreim2  10915  cjap  10917  cjdivap  10920  cnrecnv  10921  cvg1nlemcau  10995  cvg1nlemres  10996  absval  11012  rennim  11013  sqrtdiv  11053  sqrtmsq  11056  absneg  11061  abscj  11063  absval2  11068  absreim  11079  absmul  11080  absdivap  11081  absid  11082  absre  11088  absexp  11090  absexpzap  11091  absimle  11095  abssub  11112  abs3dif  11116  abs2dif  11117  abs2dif2  11118  recan  11120  cau3lem  11125  max0addsup  11230  minabs  11246  bdtrilem  11249  clim  11291  clim2  11293  clim0  11295  clim0c  11296  climi0  11299  climconst  11300  climshftlemg  11312  climcn1  11318  climcn2  11319  addcn2  11320  subcn2  11321  mulcn2  11322  reccn2ap  11323  cjcn2  11326  recn2  11327  imcn2  11328  iser3shft  11356  climcau  11357  climcvg1nlem  11359  climcvg1n  11360  serf0  11362  summodclem3  11390  summodclem2a  11391  summodc  11393  fsumf1o  11400  sumsnf  11419  fsumm1  11426  fsumcnv  11447  fsumabs  11475  fsumrelem  11481  iserabs  11485  hash2iun1dif1  11490  isumshft  11500  isumsplit  11501  expcnvap0  11512  expcnv  11514  cvgratnnlemseq  11536  cvgratnnlemrate  11540  cvgratz  11542  mertenslemub  11544  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  prodmodclem3  11585  fprodf1o  11598  prodsnf  11602  fprodm1  11608  fprodabs  11626  fprodcnv  11635  efcllemp  11668  efcj  11683  efaddlem  11684  efcan  11686  efsub  11691  efexp  11692  efzval  11693  efgt0  11694  eftlub  11700  efltim  11708  sinval  11712  cosval  11713  tanval3ap  11724  resinval  11725  recosval  11726  resin4p  11728  recos4p  11729  sinneg  11736  cosneg  11737  efmival  11743  efeul  11744  sinadd  11746  cosadd  11747  sinsub  11750  cossub  11751  addsin  11752  subsin  11753  addcos  11756  subcos  11757  sincossq  11758  sin2t  11759  cos2t  11760  sin01bnd  11767  cos01bnd  11768  sin02gt0  11773  cos12dec  11777  absefi  11778  absef  11779  absefib  11780  efieq1re  11781  demoivre  11782  demoivreALT  11783  flodddiv4  11941  alginv  12049  algcvg  12050  eucalgval  12056  eucalginv  12058  eucalglt  12059  eucalgcvga  12060  eucalg  12061  lcmgcd  12080  lcm1  12083  sqpweven  12177  2sqpwodd  12178  sqne2sq  12179  qnumval  12187  qdenval  12188  qden1elz  12207  nn0sqrtelqelz  12208  phival  12215  dfphi2  12222  phiprmpw  12224  phiprm  12225  eulerthlemth  12234  hashgcdeq  12241  phisum  12242  pythagtriplem6  12272  pythagtriplem7  12273  pythagtriplem12  12277  pythagtriplem14  12279  fldivp1  12348  ennnfonelemg  12406  ennnfonelemp1  12409  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemnn0  12425  ctinfomlemom  12430  ctiunctlemu1st  12437  ctiunctlemu2nd  12438  ctiunctlemudc  12440  ctiunctlemfo  12442  isstruct2im  12474  isstruct2r  12475  strslfv3  12510  setsslid  12515  ressbasd  12529  resseqnbasd  12534  ressplusgd  12589  ptex  12718  prdsex  12723  imasex  12731  imasival  12732  f1ocpbl  12737  f1ovscpbl  12738  imasaddvallemg  12741  qusval  12749  fvprif  12767  xpsff1o  12773  ismhm  12858  mhmpropd  12862  mhmlin  12863  mhmf1o  12866  mhmco  12879  grpinvsub  12957  mhmlem  12983  mhmid  12984  mhmmnd  12985  ghmgrp  12987  mulgfvalg  12990  mulgval  12991  mulgnegnn  12998  mulgneg  13006  mulgnegneg  13007  mulgm1  13008  mulginvcom  13013  mulgz  13016  mulgnndir  13017  mulgdir  13020  mulgass  13025  mhmmulg  13029  subgmulg  13053  isnsg  13067  eqgfval  13086  ablsub2inv  13119  mgpplusgg  13139  mgpbasg  13141  mgpscag  13142  mgptsetg  13143  mgpdsg  13145  isring  13188  ringm2neg  13237  opprmulfvalg  13247  opprsllem  13251  isunitd  13280  opprunitd  13284  invrfvald  13296  rdivmuldivd  13318  islmod  13386  islmodd  13388  scaffvalg  13401  lmodpropd  13444  lsssetm  13449  islssmd  13451  lssats2  13505  lspsnneg  13511  lspsnsub  13512  lspun0  13516  lmodindp1  13519  istps  13617  tpspropd  13621  eltpsg  13625  txvalex  13839  txval  13840  txbasval  13852  upxp  13857  uptx  13859  txrest  13861  cnmpt11  13868  cnmpt21  13876  hmeontr  13898  txhmeo  13904  psmetxrge0  13917  xmetunirn  13943  mopnval  14027  mopntopon  14028  isxms  14036  isxms2  14037  isms  14038  msrtri  14061  xmspropd  14062  mspropd  14063  setsmsbasg  14064  setsmsdsg  14065  setsmstsetg  14066  comet  14084  metcnpi  14100  metcnpi2  14101  cnbl0  14119  cnblcld  14120  resubmet  14133  elcncf  14145  cncfi  14150  rescncf  14153  mulc1cncf  14161  cncfco  14163  cncfmptid  14168  addccncf  14171  cdivcncfap  14172  negcncf  14173  mulcncflem  14175  ivthinclemlopn  14199  ivthinclemuopn  14201  limccl  14213  ellimc3apf  14214  limcimolemlt  14218  cnplimclemle  14222  limccnpcntop  14229  reldvg  14233  dvfvalap  14235  dveflem  14272  dvef  14273  sin0pilem1  14287  ef2kpi  14312  sinperlem  14314  sin2kpi  14317  cos2kpi  14318  sin2pim  14319  cos2pim  14320  ptolemy  14330  sincosq2sgn  14333  sincosq3sgn  14334  sincosq4sgn  14335  sinq12gt0  14336  tangtx  14344  sincosq1eq  14345  abssinper  14352  sinkpi  14353  coskpi  14354  cosq34lt1  14356  relogeftb  14371  relogoprlem  14374  relogexp  14378  rpcxpef  14400  logcxp  14403  1cxp  14406  ecxp  14407  rpcxpadd  14411  rpmulcxp  14415  cxpmul  14418  abscxp  14420  logsqrt  14428  rpabscxpbnd  14444  rpcxplogb  14467  lgsval  14490  lgsval2lem  14496  lgsval4a  14508  lgsdi  14523  nnsf  14839  peano4nninf  14840  peano3nninf  14841  nninfalllem1  14842  nninfall  14843  nninfsellemdc  14844  nninfsellemeq  14848  nninfsellemqall  14849  nninfsellemeqinf  14850  nninfsel  14851  exmidsbthr  14856  qdencn  14860  refeq  14861  isomninnlem  14863  apdifflemr  14880  apdiff  14881  ismkvnnlem  14885  nconstwlpolem  14898