Theorem fveq2d 5558

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 5554	. 2 |- ( A = B -> ( F ` A ) = ( F ` B ) )
3	1, 2	syl 14	1 |- ( ph -> ( F ` A ) = ( F ` B ) )

Syntax hints:   -> wi 4   = wceq 1364   ` cfv 5254

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 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262

This theorem is referenced by:  2fveq3  5559  fveq12d  5561  fveqeq2d  5562  csbfvg  5594  fvmptdf  5645  fvmptt  5649  fcof1  5826  oveq1  5925  oveq2  5926  fvoveq1d  5940  caofinvl  6155  op1stg  6203  op2ndg  6204  ot1stg  6205  ot2ndg  6206  eloprabi  6249  1stconst  6274  algrflemg  6283  tfrlem1  6361  tfrlem3ag  6362  tfrlem3a  6363  tfrlem9  6372  tfr0dm  6375  tfrlemisucaccv  6378  tfrlemiubacc  6383  tfrlemiex  6384  tfrlemi1  6385  tfr1onlem3ag  6390  tfr1onlemsucaccv  6394  tfr1onlemubacc  6399  tfr1onlemex  6400  tfr1onlemaccex  6401  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllemubacc  6412  tfrcllemex  6413  tfrcllemaccex  6414  tfrcllemres  6415  tfrcldm  6416  rdgivallem  6434  rdgival  6435  rdgss  6436  rdgisuc1  6437  rdgon  6439  rdg0  6440  frec0g  6450  frecabcl  6452  freccllem  6455  frecfcllem  6457  frecsuclem  6459  frecsuc  6460  frecrdg  6461  oav2  6516  omv2  6518  xpdom2  6885  xpmapenlem  6905  xpmapen  6906  ac6sfi  6954  1stinl  7133  2ndinl  7134  1stinr  7135  2ndinr  7136  updjudhcoinlf  7139  updjudhcoinrg  7140  caseinl  7150  caseinr  7151  omp1eomlem  7153  omp1eom  7154  difinfsn  7159  ctmlemr  7167  ctm  7168  ctssdclemn0  7169  ctssdccl  7170  nninfninc  7182  nnnninfeq  7187  nnnninfeq2  7188  enomnilem  7197  enmkvlem  7220  enwomnilem  7228  exmidfodomrlemeldju  7259  exmidfodomrlemreseldju  7260  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  cc2  7327  cc3  7328  ltdfpr  7566  genpelvl  7572  genpelvu  7573  recexpr  7698  cauappcvgprlem1  7719  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemcl  7736  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprlem1  7739  caucvgprlem2  7740  caucvgpr  7742  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemnkeqj  7750  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemloc  7763  caucvgprprlemclphr  7765  caucvgprprlemexbt  7766  caucvgprprlem1  7769  caucvgprprlem2  7770  caucvgsr  7862  axcaucvglemval  7957  axcaucvglemres  7959  fv0p1e1  9097  uzin  9625  cnref1o  9716  fzsuc2  10145  fseq1m1p1  10161  fzoss2  10239  elfzonlteqm1  10277  divfl0  10365  flqzadd  10367  fldiv4p1lem1div2  10374  ceilqval  10377  flqdiv  10392  modqval  10395  modqfrac  10408  modqmulnn  10413  modqid  10420  modqcyc  10430  modqdi  10463  frec2uzuzd  10473  frec2uzrdg  10480  frecuzrdgrcl  10481  frecuzrdgtcl  10483  frecuzrdgsuc  10485  frecuzrdgrclt  10486  frecuzrdgg  10487  frecuzrdgfunlem  10490  frecuzrdgsuctlem  10494  iseqovex  10529  iseqvalcbv  10530  seq3val  10531  seqvalcd  10532  seq3m1  10544  seq3shft2  10552  seqshft2g  10553  monoord  10556  monoord2  10557  iseqf1olemqval  10571  iseqf1olemab  10573  iseqf1olemqk  10578  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  iseqf1olemfvp  10581  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seq3f1olemp  10586  seq3f1oleml  10587  seqf1oglem1  10590  seqf1oglem2  10591  seqf1og  10592  seq3homo  10598  seqhomog  10601  exp3val  10612  expnegap0  10618  facnn2  10805  facwordi  10811  faclbnd6  10815  bcval  10820  bccmpl  10825  bcn0  10826  bcm1k  10831  bcp1n  10832  bcn2  10835  hashinfom  10849  hashennn  10851  hashsng  10869  omgadd  10873  hashprg  10879  fihashssdif  10889  hashdifpr  10891  hashfzo  10893  hashfzp1  10895  hashxp  10897  zfz1isolemiso  10910  zfz1iso  10912  shftval2  10970  shftval3  10971  shftval4  10972  shftval5  10973  seq3shft  10982  imval  10994  imre  10995  reim  10996  crim  11002  reim0  11005  mulreap  11008  recj  11011  reneg  11012  readd  11013  resub  11014  remullem  11015  redivap  11018  imcj  11019  imneg  11020  imadd  11021  imsub  11022  imdivap  11025  cjsub  11036  cjexp  11037  cjreim2  11048  cjap  11050  cjdivap  11053  cnrecnv  11054  cvg1nlemcau  11128  cvg1nlemres  11129  absval  11145  rennim  11146  sqrtdiv  11186  sqrtmsq  11189  absneg  11194  abscj  11196  absval2  11201  absreim  11212  absmul  11213  absdivap  11214  absid  11215  absre  11221  absexp  11223  absexpzap  11224  absimle  11228  abssub  11245  abs3dif  11249  abs2dif  11250  abs2dif2  11251  recan  11253  cau3lem  11258  max0addsup  11363  minabs  11379  bdtrilem  11382  clim  11424  clim2  11426  clim0  11428  clim0c  11429  climi0  11432  climconst  11433  climshftlemg  11445  climcn1  11451  climcn2  11452  addcn2  11453  subcn2  11454  mulcn2  11455  reccn2ap  11456  cjcn2  11459  recn2  11460  imcn2  11461  iser3shft  11489  climcau  11490  climcvg1nlem  11492  climcvg1n  11493  serf0  11495  summodclem3  11523  summodclem2a  11524  summodc  11526  fsumf1o  11533  sumsnf  11552  fsumm1  11559  fsumcnv  11580  fsumabs  11608  fsumrelem  11614  iserabs  11618  hash2iun1dif1  11623  isumshft  11633  isumsplit  11634  expcnvap0  11645  expcnv  11647  cvgratnnlemseq  11669  cvgratnnlemrate  11673  cvgratz  11675  mertenslemub  11677  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  prodmodclem3  11718  fprodf1o  11731  prodsnf  11735  fprodm1  11741  fprodabs  11759  fprodcnv  11768  efcllemp  11801  efcj  11816  efaddlem  11817  efcan  11819  efsub  11824  efexp  11825  efzval  11826  efgt0  11827  eftlub  11833  efltim  11841  sinval  11845  cosval  11846  tanval3ap  11857  resinval  11858  recosval  11859  resin4p  11861  recos4p  11862  sinneg  11869  cosneg  11870  efmival  11876  efeul  11877  sinadd  11879  cosadd  11880  sinsub  11883  cossub  11884  addsin  11885  subsin  11886  addcos  11889  subcos  11890  sincossq  11891  sin2t  11892  cos2t  11893  sin01bnd  11900  cos01bnd  11901  sin02gt0  11907  cos12dec  11911  absefi  11912  absef  11913  absefib  11914  efieq1re  11915  demoivre  11916  demoivreALT  11917  flodddiv4  12075  nninfctlemfo  12177  alginv  12185  algcvg  12186  eucalgval  12192  eucalginv  12194  eucalglt  12195  eucalgcvga  12196  eucalg  12197  lcmgcd  12216  lcm1  12219  sqpweven  12313  2sqpwodd  12314  sqne2sq  12315  qnumval  12323  qdenval  12324  qden1elz  12343  nn0sqrtelqelz  12344  phival  12351  dfphi2  12358  phiprmpw  12360  phiprm  12361  eulerthlemth  12370  hashgcdeq  12377  phisum  12378  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem12  12413  pythagtriplem14  12415  fldivp1  12486  4sqlem11  12539  ennnfonelemg  12560  ennnfonelemp1  12563  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemnn0  12579  ctinfomlemom  12584  ctiunctlemu1st  12591  ctiunctlemu2nd  12592  ctiunctlemudc  12594  ctiunctlemfo  12596  isstruct2im  12628  isstruct2r  12629  strslfv3  12664  setsslid  12669  ressbasd  12685  resseqnbasd  12691  ressplusgd  12746  ptex  12875  prdsex  12880  imasex  12888  imasival  12889  f1ocpbl  12894  f1ovscpbl  12895  imasaddvallemg  12898  qusval  12906  fvprif  12926  xpsff1o  12932  igsumvalx  12972  gsumprval  12982  ismhm  13033  mhmpropd  13038  mhmlin  13039  mhmf1o  13042  resmhm  13059  mhmco  13062  gsumwmhm  13070  grpinvsub  13154  imasgrp2  13180  imasgrp  13181  mhmlem  13184  mhmid  13185  mhmmnd  13186  ghmgrp  13188  mulgfvalg  13191  mulgval  13192  mulgnegnn  13202  mulgneg  13210  mulgnegneg  13211  mulgm1  13212  mulginvcom  13217  mulgz  13220  mulgnndir  13221  mulgdir  13224  mulgass  13229  mhmmulg  13233  subgmulg  13258  isnsg  13272  eqgfval  13292  ghmlin  13318  ghmid  13319  ghminv  13320  ghmsub  13321  ghmmulg  13326  resghm  13330  ghmeql  13337  ablsub2inv  13381  ghmcmn  13397  invghm  13399  imasabl  13406  gsumfzreidx  13407  gsumfzmhm  13413  mgpplusgg  13420  mgpbasg  13422  mgpscag  13423  mgptsetg  13424  mgpdsg  13426  rngm2neg  13445  imasrng  13452  isring  13496  ringm2neg  13551  imasring  13560  opprmulfvalg  13566  opprsllem  13570  isunitd  13602  opprunitd  13606  invrfvald  13618  rdivmuldivd  13640  rhmmul  13660  isrhm2d  13661  rhm1  13663  rhmdvdsr  13671  rhmopp  13672  rhmunitinv  13674  islmod  13787  islmodd  13789  scaffvalg  13802  lmodpropd  13845  lsssetm  13852  islssmd  13855  lssats2  13910  lspsnneg  13916  lspsnsub  13917  lspun0  13921  lmodindp1  13924  sralemg  13934  srascag  13938  sravscag  13939  sraipg  13940  rlmscabas  13956  ixpsnbasval  13962  2idlval  13998  2idlvalg  13999  mulgrhm2  14098  zlmlemg  14116  zlmsca  14120  zlmvscag  14121  znval  14124  znle  14125  znbaslemnn  14127  znidomb  14146  psrval  14152  psrbasg  14159  psrplusgg  14162  istps  14200  tpspropd  14204  eltpsg  14208  txvalex  14422  txval  14423  txbasval  14435  upxp  14440  uptx  14442  txrest  14444  cnmpt11  14451  cnmpt21  14459  hmeontr  14481  txhmeo  14487  psmetxrge0  14500  xmetunirn  14526  mopnval  14610  mopntopon  14611  isxms  14619  isxms2  14620  isms  14621  msrtri  14644  xmspropd  14645  mspropd  14646  setsmsbasg  14647  setsmsdsg  14648  setsmstsetg  14649  comet  14667  metcnpi  14683  metcnpi2  14684  cnbl0  14702  cnblcld  14703  resubmet  14716  elcncf  14728  cncfi  14733  rescncf  14736  mulc1cncf  14744  cncfco  14746  cncfmptid  14751  addccncf  14754  cdivcncfap  14758  negcncf  14759  mulcncflem  14761  ivthinclemlopn  14790  ivthinclemuopn  14792  limccl  14813  ellimc3apf  14814  limcimolemlt  14818  cnplimclemle  14822  limccnpcntop  14829  reldvg  14833  dvfvalap  14835  dveflem  14872  dvef  14873  plymullem1  14894  sin0pilem1  14916  ef2kpi  14941  sinperlem  14943  sin2kpi  14946  cos2kpi  14947  sin2pim  14948  cos2pim  14949  ptolemy  14959  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  sinq12gt0  14965  tangtx  14973  sincosq1eq  14974  abssinper  14981  sinkpi  14982  coskpi  14983  cosq34lt1  14985  relogeftb  15000  relogoprlem  15003  relogexp  15007  rpcxpef  15029  logcxp  15032  1cxp  15035  ecxp  15036  rpcxpadd  15040  rpmulcxp  15044  cxpmul  15047  abscxp  15049  logsqrt  15057  rpabscxpbnd  15073  rpcxplogb  15096  lgsval  15120  lgsval2lem  15126  lgsval4a  15138  lgsdi  15153  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191  nnsf  15495  peano4nninf  15496  peano3nninf  15497  nninfalllem1  15498  nninfall  15499  nninfsellemdc  15500  nninfsellemeq  15504  nninfsellemqall  15505  nninfsellemeqinf  15506  nninfsel  15507  exmidsbthr  15513  qdencn  15517  refeq  15518  isomninnlem  15520  apdifflemr  15537  apdiff  15538  ismkvnnlem  15542  nconstwlpolem  15555