Theorem fveq2d 5202

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

Syntax hints:   -> wi 4   = wceq 1284   ` cfv 4922

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930

This theorem is referenced by:  fveq12d  5204  csbfvg  5232  fvmptdf  5279  fvmptt  5283  fcof1  5443  oveq1  5539  oveq2  5540  caofinvl  5753  op1stg  5797  op2ndg  5798  ot1stg  5799  ot2ndg  5800  eloprabi  5842  1stconst  5862  algrflemg  5871  tfrlem1  5946  tfrlem3ag  5947  tfrlem3a  5948  tfrlem9  5958  tfr0  5960  tfrlemisucaccv  5962  tfrlemiubacc  5967  tfrlemiex  5968  tfrlemi1  5969  rdgivallem  5991  rdgival  5992  rdgss  5993  rdgisuc1  5994  rdg0  5997  frec0g  6006  frecsuclem3  6013  frecsuc  6014  frecrdg  6015  oav2  6066  omv2  6068  xpdom2  6328  ac6sfi  6379  ltdfpr  6696  genpelvl  6702  genpelvu  6703  recexpr  6828  cauappcvgprlem1  6849  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemm  6858  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemcl  6866  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgprlem2  6870  caucvgpr  6872  caucvgprprlemell  6875  caucvgprprlemelu  6876  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemnkeqj  6880  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemloc  6893  caucvgprprlemclphr  6895  caucvgprprlemexbt  6896  caucvgprprlem1  6899  caucvgprprlem2  6900  caucvgsr  6978  axcaucvglemval  7063  axcaucvglemres  7065  uzin  8651  cnref1o  8733  fzsuc2  9096  fseq1m1p1  9112  fzoss2  9181  elfzonlteqm1  9219  divfl0  9298  flqzadd  9300  fldiv4p1lem1div2  9307  ceilqval  9308  flqdiv  9323  modqval  9326  modqfrac  9339  modqmulnn  9344  modqid  9351  modqcyc  9361  modqdi  9394  frec2uzzd  9402  frec2uzuzd  9404  frec2uzrdg  9411  frecuzrdgfn  9414  frecuzrdgsuc  9417  iseqovex  9439  iseqval  9440  iseqp1  9445  iseqm1  9447  iseqshft2  9452  monoord  9455  monoord2  9456  iseqhomo  9468  expival  9478  expnegap0  9484  facp1  9657  facnn2  9661  facwordi  9667  faclbnd6  9671  bcval  9676  bccmpl  9681  bcn0  9682  bcm1k  9687  bcp1n  9688  bcn2  9691  shftval2  9714  shftval3  9715  shftval4  9716  shftval5  9717  imval  9737  imre  9738  reim  9739  crim  9745  reim0  9748  mulreap  9751  recj  9754  reneg  9755  readd  9756  resub  9757  remullem  9758  redivap  9761  imcj  9762  imneg  9763  imadd  9764  imsub  9765  imdivap  9768  cjsub  9779  cjexp  9780  cjreim2  9791  cjap  9793  cjdivap  9796  cnrecnv  9797  cvg1nlemcau  9870  cvg1nlemres  9871  absval  9887  rennim  9888  sqrtdiv  9928  sqrtmsq  9931  absneg  9936  abscj  9938  absval2  9943  absreim  9954  absmul  9955  absdivap  9956  absid  9957  absre  9963  absexp  9965  absexpzap  9966  absimle  9970  abssub  9987  abs3dif  9991  abs2dif  9992  abs2dif2  9993  recan  9995  cau3lem  10000  max0addsup  10105  clim  10120  clim2  10122  clim0  10124  clim0c  10125  climi0  10128  climconst  10129  climshftlemg  10141  climcn1  10147  climcn2  10148  addcn2  10149  subcn2  10150  mulcn2  10151  cjcn2  10154  recn2  10155  imcn2  10156  climcau  10184  climcvg1nlem  10186  climcvg1n  10187  serif0  10189  flodddiv4  10334  ialginv  10429  ialgcvg  10430  ialgcvga  10433  eucalgval  10436  eucalginv  10438  eucalglt  10439  eucialgcvga  10440  eucialg  10441  lcmgcd  10460  lcm1  10463  sqpweven  10553  2sqpwodd  10554  sqne2sq  10555  qdencn  10785