Theorem fveq2d 5357

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

Syntax hints:   -> wi 4   = wceq 1299   ` cfv 5059

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-rex 2381  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-iota 5024  df-fv 5067

This theorem is referenced by:  2fveq3  5358  fveq12d  5360  fveqeq2d  5361  csbfvg  5391  fvmptdf  5440  fvmptt  5444  fcof1  5616  oveq1  5713  oveq2  5714  fvoveq1d  5728  caofinvl  5935  op1stg  5979  op2ndg  5980  ot1stg  5981  ot2ndg  5982  eloprabi  6024  1stconst  6048  algrflemg  6057  tfrlem1  6135  tfrlem3ag  6136  tfrlem3a  6137  tfrlem9  6146  tfr0dm  6149  tfrlemisucaccv  6152  tfrlemiubacc  6157  tfrlemiex  6158  tfrlemi1  6159  tfr1onlem3ag  6164  tfr1onlemsucaccv  6168  tfr1onlemubacc  6173  tfr1onlemex  6174  tfr1onlemaccex  6175  tfrcllemsucaccv  6181  tfrcllembxssdm  6183  tfrcllemubacc  6186  tfrcllemex  6187  tfrcllemaccex  6188  tfrcllemres  6189  tfrcldm  6190  rdgivallem  6208  rdgival  6209  rdgss  6210  rdgisuc1  6211  rdgon  6213  rdg0  6214  frec0g  6224  frecabcl  6226  freccllem  6229  frecfcllem  6231  frecsuclem  6233  frecsuc  6234  frecrdg  6235  oav2  6289  omv2  6291  xpdom2  6654  xpmapenlem  6672  xpmapen  6673  ac6sfi  6721  1stinl  6874  2ndinl  6875  1stinr  6876  2ndinr  6877  updjudhcoinlf  6880  updjudhcoinrg  6881  caseinl  6891  caseinr  6892  omp1eomlem  6894  omp1eom  6895  difinfsn  6900  ctmlemr  6908  ctm  6909  ctssdclemn0  6910  ctssdclemr  6911  enomnilem  6922  exmidfodomrlemeldju  6964  exmidfodomrlemreseldju  6965  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  ltdfpr  7215  genpelvl  7221  genpelvu  7222  recexpr  7347  cauappcvgprlem1  7368  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemm  7377  caucvgprlemdisj  7383  caucvgprlemloc  7384  caucvgprlemcl  7385  caucvgprlemladdfu  7386  caucvgprlemladdrl  7387  caucvgprlem1  7388  caucvgprlem2  7389  caucvgpr  7391  caucvgprprlemell  7394  caucvgprprlemelu  7395  caucvgprprlemcbv  7396  caucvgprprlemval  7397  caucvgprprlemnkeqj  7399  caucvgprprlemmu  7404  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemopu  7408  caucvgprprlemloc  7412  caucvgprprlemclphr  7414  caucvgprprlemexbt  7415  caucvgprprlem1  7418  caucvgprprlem2  7419  caucvgsr  7497  axcaucvglemval  7582  axcaucvglemres  7584  fv0p1e1  8693  uzin  9208  cnref1o  9290  fzsuc2  9700  fseq1m1p1  9716  fzoss2  9790  elfzonlteqm1  9828  divfl0  9910  flqzadd  9912  fldiv4p1lem1div2  9919  ceilqval  9920  flqdiv  9935  modqval  9938  modqfrac  9951  modqmulnn  9956  modqid  9963  modqcyc  9973  modqdi  10006  frec2uzuzd  10016  frec2uzrdg  10023  frecuzrdgrcl  10024  frecuzrdgtcl  10026  frecuzrdgsuc  10028  frecuzrdgrclt  10029  frecuzrdgg  10030  frecuzrdgfunlem  10033  frecuzrdgsuctlem  10037  iseqovex  10070  iseqvalcbv  10071  seq3val  10072  seqvalcd  10073  seq3m1  10082  seq3shft2  10087  monoord  10090  monoord2  10091  iseqf1olemqval  10101  iseqf1olemab  10103  iseqf1olemqk  10108  iseqf1olemjpcl  10109  iseqf1olemqpcl  10110  iseqf1olemfvp  10111  seq3f1olemqsumkj  10112  seq3f1olemqsumk  10113  seq3f1olemqsum  10114  seq3f1olemp  10116  seq3f1oleml  10117  seq3homo  10124  exp3val  10136  expnegap0  10142  facnn2  10321  facwordi  10327  faclbnd6  10331  bcval  10336  bccmpl  10341  bcn0  10342  bcm1k  10347  bcp1n  10348  bcn2  10351  hashinfom  10365  hashennn  10367  hashsng  10385  omgadd  10389  hashprg  10395  fihashssdif  10405  hashdifpr  10407  hashfzo  10409  hashfzp1  10411  hashxp  10413  zfz1isolemiso  10423  zfz1iso  10425  shftval2  10439  shftval3  10440  shftval4  10441  shftval5  10442  seq3shft  10451  imval  10463  imre  10464  reim  10465  crim  10471  reim0  10474  mulreap  10477  recj  10480  reneg  10481  readd  10482  resub  10483  remullem  10484  redivap  10487  imcj  10488  imneg  10489  imadd  10490  imsub  10491  imdivap  10494  cjsub  10505  cjexp  10506  cjreim2  10517  cjap  10519  cjdivap  10522  cnrecnv  10523  cvg1nlemcau  10596  cvg1nlemres  10597  absval  10613  rennim  10614  sqrtdiv  10654  sqrtmsq  10657  absneg  10662  abscj  10664  absval2  10669  absreim  10680  absmul  10681  absdivap  10682  absid  10683  absre  10689  absexp  10691  absexpzap  10692  absimle  10696  abssub  10713  abs3dif  10717  abs2dif  10718  abs2dif2  10719  recan  10721  cau3lem  10726  max0addsup  10831  minabs  10846  bdtrilem  10849  clim  10889  clim2  10891  clim0  10893  clim0c  10894  climi0  10897  climconst  10898  climshftlemg  10910  climcn1  10916  climcn2  10917  addcn2  10918  subcn2  10919  mulcn2  10920  reccn2ap  10921  cjcn2  10924  recn2  10925  imcn2  10926  iser3shft  10954  climcau  10955  climcvg1nlem  10957  climcvg1n  10958  serf0  10960  summodclem3  10988  summodclem2a  10989  summodc  10991  fsumf1o  10998  sumsnf  11017  fsumm1  11024  fsumcnv  11045  fsumabs  11073  fsumrelem  11079  iserabs  11083  hash2iun1dif1  11088  isumshft  11098  isumsplit  11099  expcnvap0  11110  expcnv  11112  cvgratnnlemseq  11134  cvgratnnlemrate  11138  cvgratz  11140  mertenslemub  11142  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  efcllemp  11162  efcj  11177  efaddlem  11178  efcan  11180  efsub  11185  efexp  11186  efzval  11187  efgt0  11188  eftlub  11194  efltim  11202  sinval  11207  cosval  11208  tanval3ap  11219  resinval  11220  recosval  11221  resin4p  11223  recos4p  11224  sinneg  11231  cosneg  11232  efmival  11238  efeul  11239  sinadd  11241  cosadd  11242  sinsub  11245  cossub  11246  addsin  11247  subsin  11248  addcos  11251  subcos  11252  sincossq  11253  sin2t  11254  cos2t  11255  sin01bnd  11262  cos01bnd  11263  sin02gt0  11268  absefi  11272  absef  11273  absefib  11274  efieq1re  11275  demoivre  11276  demoivreALT  11277  flodddiv4  11426  alginv  11521  algcvg  11522  eucalgval  11528  eucalginv  11530  eucalglt  11531  eucalgcvga  11532  eucalg  11533  lcmgcd  11552  lcm1  11555  sqpweven  11645  2sqpwodd  11646  sqne2sq  11647  qnumval  11655  qdenval  11656  qden1elz  11675  nn0sqrtelqelz  11676  phival  11681  dfphi2  11688  phiprmpw  11690  phiprm  11691  hashgcdeq  11696  ennnfonelemg  11708  ennnfonelemp1  11711  ennnfonelemkh  11717  ennnfonelemhf1o  11718  ennnfonelemnn0  11727  ctinfomlemom  11732  isstruct2im  11751  isstruct2r  11752  strslfv3  11786  setsslid  11791  ressid2  11800  ressval2  11801  istps  11981  tpspropd  11985  eltpsg  11989  txvalex  12204  txval  12205  txbasval  12217  upxp  12222  uptx  12224  txrest  12226  cnmpt11  12233  cnmpt21  12241  psmetxrge0  12260  xmetunirn  12286  mopnval  12370  mopntopon  12371  isxms  12379  isxms2  12380  isms  12381  msrtri  12404  xmspropd  12405  mspropd  12406  setsmsbasg  12407  setsmsdsg  12408  setsmstsetg  12409  comet  12427  metcnpi  12439  metcnpi2  12440  cnbl0  12456  cnblcld  12457  resubmet  12467  elcncf  12473  cncfi  12478  rescncf  12481  mulc1cncf  12489  cncfco  12491  cncfmptid  12496  addccncf  12498  cdivcncfap  12499  negcncf  12500  mulcncflem  12502  limccl  12510  ellimc3ap  12511  limcimolemlt  12513  limccnpcntop  12520  reldvg  12521  dvfvalap  12523  nnsf  12783  peano4nninf  12784  peano3nninf  12785  nninfalllemn  12786  nninfalllem1  12787  nninfall  12788  nninfsellemdc  12790  nninfsellemeq  12794  nninfsellemqall  12795  nninfsellemeqinf  12796  nninfsel  12797  nninfomni  12799  exmidsbthr  12802  qdencn  12806  refeq  12807  isomninnlem  12809