Theorem fveq2d 5516

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 5512	. 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 5213

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 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-br 4002  df-iota 5175  df-fv 5221

This theorem is referenced by:  2fveq3  5517  fveq12d  5519  fveqeq2d  5520  csbfvg  5550  fvmptdf  5600  fvmptt  5604  fcof1  5779  oveq1  5877  oveq2  5878  fvoveq1d  5892  caofinvl  6100  op1stg  6146  op2ndg  6147  ot1stg  6148  ot2ndg  6149  eloprabi  6192  1stconst  6217  algrflemg  6226  tfrlem1  6304  tfrlem3ag  6305  tfrlem3a  6306  tfrlem9  6315  tfr0dm  6318  tfrlemisucaccv  6321  tfrlemiubacc  6326  tfrlemiex  6327  tfrlemi1  6328  tfr1onlem3ag  6333  tfr1onlemsucaccv  6337  tfr1onlemubacc  6342  tfr1onlemex  6343  tfr1onlemaccex  6344  tfrcllemsucaccv  6350  tfrcllembxssdm  6352  tfrcllemubacc  6355  tfrcllemex  6356  tfrcllemaccex  6357  tfrcllemres  6358  tfrcldm  6359  rdgivallem  6377  rdgival  6378  rdgss  6379  rdgisuc1  6380  rdgon  6382  rdg0  6383  frec0g  6393  frecabcl  6395  freccllem  6398  frecfcllem  6400  frecsuclem  6402  frecsuc  6403  frecrdg  6404  oav2  6459  omv2  6461  xpdom2  6826  xpmapenlem  6844  xpmapen  6845  ac6sfi  6893  1stinl  7068  2ndinl  7069  1stinr  7070  2ndinr  7071  updjudhcoinlf  7074  updjudhcoinrg  7075  caseinl  7085  caseinr  7086  omp1eomlem  7088  omp1eom  7089  difinfsn  7094  ctmlemr  7102  ctm  7103  ctssdclemn0  7104  ctssdccl  7105  nnnninfeq  7121  nnnninfeq2  7122  enomnilem  7131  enmkvlem  7154  enwomnilem  7162  exmidfodomrlemeldju  7193  exmidfodomrlemreseldju  7194  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  exmidaclem  7202  cc2  7261  cc3  7262  ltdfpr  7500  genpelvl  7506  genpelvu  7507  recexpr  7632  cauappcvgprlem1  7653  caucvgprlemnkj  7660  caucvgprlemnbj  7661  caucvgprlemm  7662  caucvgprlemdisj  7668  caucvgprlemloc  7669  caucvgprlemcl  7670  caucvgprlemladdfu  7671  caucvgprlemladdrl  7672  caucvgprlem1  7673  caucvgprlem2  7674  caucvgpr  7676  caucvgprprlemell  7679  caucvgprprlemelu  7680  caucvgprprlemcbv  7681  caucvgprprlemval  7682  caucvgprprlemnkeqj  7684  caucvgprprlemmu  7689  caucvgprprlemopl  7691  caucvgprprlemlol  7692  caucvgprprlemopu  7693  caucvgprprlemloc  7697  caucvgprprlemclphr  7699  caucvgprprlemexbt  7700  caucvgprprlem1  7703  caucvgprprlem2  7704  caucvgsr  7796  axcaucvglemval  7891  axcaucvglemres  7893  fv0p1e1  9028  uzin  9554  cnref1o  9644  fzsuc2  10072  fseq1m1p1  10088  fzoss2  10165  elfzonlteqm1  10203  divfl0  10289  flqzadd  10291  fldiv4p1lem1div2  10298  ceilqval  10299  flqdiv  10314  modqval  10317  modqfrac  10330  modqmulnn  10335  modqid  10342  modqcyc  10352  modqdi  10385  frec2uzuzd  10395  frec2uzrdg  10402  frecuzrdgrcl  10403  frecuzrdgtcl  10405  frecuzrdgsuc  10407  frecuzrdgrclt  10408  frecuzrdgg  10409  frecuzrdgfunlem  10412  frecuzrdgsuctlem  10416  iseqovex  10449  iseqvalcbv  10450  seq3val  10451  seqvalcd  10452  seq3m1  10461  seq3shft2  10466  monoord  10469  monoord2  10470  iseqf1olemqval  10480  iseqf1olemab  10482  iseqf1olemqk  10487  iseqf1olemjpcl  10488  iseqf1olemqpcl  10489  iseqf1olemfvp  10490  seq3f1olemqsumkj  10491  seq3f1olemqsumk  10492  seq3f1olemqsum  10493  seq3f1olemp  10495  seq3f1oleml  10496  seq3homo  10503  exp3val  10515  expnegap0  10521  facnn2  10705  facwordi  10711  faclbnd6  10715  bcval  10720  bccmpl  10725  bcn0  10726  bcm1k  10731  bcp1n  10732  bcn2  10735  hashinfom  10749  hashennn  10751  hashsng  10769  omgadd  10773  hashprg  10779  fihashssdif  10789  hashdifpr  10791  hashfzo  10793  hashfzp1  10795  hashxp  10797  zfz1isolemiso  10810  zfz1iso  10812  shftval2  10826  shftval3  10827  shftval4  10828  shftval5  10829  seq3shft  10838  imval  10850  imre  10851  reim  10852  crim  10858  reim0  10861  mulreap  10864  recj  10867  reneg  10868  readd  10869  resub  10870  remullem  10871  redivap  10874  imcj  10875  imneg  10876  imadd  10877  imsub  10878  imdivap  10881  cjsub  10892  cjexp  10893  cjreim2  10904  cjap  10906  cjdivap  10909  cnrecnv  10910  cvg1nlemcau  10984  cvg1nlemres  10985  absval  11001  rennim  11002  sqrtdiv  11042  sqrtmsq  11045  absneg  11050  abscj  11052  absval2  11057  absreim  11068  absmul  11069  absdivap  11070  absid  11071  absre  11077  absexp  11079  absexpzap  11080  absimle  11084  abssub  11101  abs3dif  11105  abs2dif  11106  abs2dif2  11107  recan  11109  cau3lem  11114  max0addsup  11219  minabs  11235  bdtrilem  11238  clim  11280  clim2  11282  clim0  11284  clim0c  11285  climi0  11288  climconst  11289  climshftlemg  11301  climcn1  11307  climcn2  11308  addcn2  11309  subcn2  11310  mulcn2  11311  reccn2ap  11312  cjcn2  11315  recn2  11316  imcn2  11317  iser3shft  11345  climcau  11346  climcvg1nlem  11348  climcvg1n  11349  serf0  11351  summodclem3  11379  summodclem2a  11380  summodc  11382  fsumf1o  11389  sumsnf  11408  fsumm1  11415  fsumcnv  11436  fsumabs  11464  fsumrelem  11470  iserabs  11474  hash2iun1dif1  11479  isumshft  11489  isumsplit  11490  expcnvap0  11501  expcnv  11503  cvgratnnlemseq  11525  cvgratnnlemrate  11529  cvgratz  11531  mertenslemub  11533  mertenslemi1  11534  mertenslem2  11535  mertensabs  11536  prodmodclem3  11574  fprodf1o  11587  prodsnf  11591  fprodm1  11597  fprodabs  11615  fprodcnv  11624  efcllemp  11657  efcj  11672  efaddlem  11673  efcan  11675  efsub  11680  efexp  11681  efzval  11682  efgt0  11683  eftlub  11689  efltim  11697  sinval  11701  cosval  11702  tanval3ap  11713  resinval  11714  recosval  11715  resin4p  11717  recos4p  11718  sinneg  11725  cosneg  11726  efmival  11732  efeul  11733  sinadd  11735  cosadd  11736  sinsub  11739  cossub  11740  addsin  11741  subsin  11742  addcos  11745  subcos  11746  sincossq  11747  sin2t  11748  cos2t  11749  sin01bnd  11756  cos01bnd  11757  sin02gt0  11762  cos12dec  11766  absefi  11767  absef  11768  absefib  11769  efieq1re  11770  demoivre  11771  demoivreALT  11772  flodddiv4  11929  alginv  12037  algcvg  12038  eucalgval  12044  eucalginv  12046  eucalglt  12047  eucalgcvga  12048  eucalg  12049  lcmgcd  12068  lcm1  12071  sqpweven  12165  2sqpwodd  12166  sqne2sq  12167  qnumval  12175  qdenval  12176  qden1elz  12195  nn0sqrtelqelz  12196  phival  12203  dfphi2  12210  phiprmpw  12212  phiprm  12213  eulerthlemth  12222  hashgcdeq  12229  phisum  12230  pythagtriplem6  12260  pythagtriplem7  12261  pythagtriplem12  12265  pythagtriplem14  12267  fldivp1  12336  ennnfonelemg  12394  ennnfonelemp1  12397  ennnfonelemkh  12403  ennnfonelemhf1o  12404  ennnfonelemnn0  12413  ctinfomlemom  12418  ctiunctlemu1st  12425  ctiunctlemu2nd  12426  ctiunctlemudc  12428  ctiunctlemfo  12430  isstruct2im  12462  isstruct2r  12463  strslfv3  12498  setsslid  12503  ressbasd  12517  resseqnbasd  12522  ressplusgd  12577  ismhm  12781  mhmpropd  12785  mhmlin  12786  mhmf1o  12789  mhmco  12802  grpinvsub  12880  mhmlem  12906  mhmid  12907  mhmmnd  12908  ghmgrp  12910  mulgfvalg  12913  mulgval  12914  mulgnegnn  12921  mulgneg  12929  mulgnegneg  12930  mulgm1  12931  mulginvcom  12935  mulgz  12938  mulgnndir  12939  mulgdir  12942  mulgass  12947  mhmmulg  12951  subgmulg  12974  ablsub2inv  13014  mgpplusgg  13034  mgpbasg  13036  mgpscag  13037  mgptsetg  13038  mgpdsg  13040  isring  13083  ringm2neg  13132  opprmulfvalg  13141  opprsllem  13145  isunitd  13174  opprunitd  13178  invrfvald  13190  rdivmuldivd  13212  istps  13312  tpspropd  13316  eltpsg  13320  txvalex  13536  txval  13537  txbasval  13549  upxp  13554  uptx  13556  txrest  13558  cnmpt11  13565  cnmpt21  13573  hmeontr  13595  txhmeo  13601  psmetxrge0  13614  xmetunirn  13640  mopnval  13724  mopntopon  13725  isxms  13733  isxms2  13734  isms  13735  msrtri  13758  xmspropd  13759  mspropd  13760  setsmsbasg  13761  setsmsdsg  13762  setsmstsetg  13763  comet  13781  metcnpi  13797  metcnpi2  13798  cnbl0  13816  cnblcld  13817  resubmet  13830  elcncf  13842  cncfi  13847  rescncf  13850  mulc1cncf  13858  cncfco  13860  cncfmptid  13865  addccncf  13868  cdivcncfap  13869  negcncf  13870  mulcncflem  13872  ivthinclemlopn  13896  ivthinclemuopn  13898  limccl  13910  ellimc3apf  13911  limcimolemlt  13915  cnplimclemle  13919  limccnpcntop  13926  reldvg  13930  dvfvalap  13932  dveflem  13969  dvef  13970  sin0pilem1  13984  ef2kpi  14009  sinperlem  14011  sin2kpi  14014  cos2kpi  14015  sin2pim  14016  cos2pim  14017  ptolemy  14027  sincosq2sgn  14030  sincosq3sgn  14031  sincosq4sgn  14032  sinq12gt0  14033  tangtx  14041  sincosq1eq  14042  abssinper  14049  sinkpi  14050  coskpi  14051  cosq34lt1  14053  relogeftb  14068  relogoprlem  14071  relogexp  14075  rpcxpef  14097  logcxp  14100  1cxp  14103  ecxp  14104  rpcxpadd  14108  rpmulcxp  14112  cxpmul  14115  abscxp  14117  logsqrt  14125  rpabscxpbnd  14141  rpcxplogb  14164  lgsval  14187  lgsval2lem  14193  lgsval4a  14205  lgsdi  14220  nnsf  14525  peano4nninf  14526  peano3nninf  14527  nninfalllem1  14528  nninfall  14529  nninfsellemdc  14530  nninfsellemeq  14534  nninfsellemqall  14535  nninfsellemeqinf  14536  nninfsel  14537  exmidsbthr  14542  qdencn  14546  refeq  14547  isomninnlem  14549  apdifflemr  14566  apdiff  14567  ismkvnnlem  14571  nconstwlpolem  14583