Theorem fveq2d 5519

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 5515	. 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 5216

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 3810  df-br 4004  df-iota 5178  df-fv 5224

This theorem is referenced by:  2fveq3  5520  fveq12d  5522  fveqeq2d  5523  csbfvg  5553  fvmptdf  5603  fvmptt  5607  fcof1  5783  oveq1  5881  oveq2  5882  fvoveq1d  5896  caofinvl  6104  op1stg  6150  op2ndg  6151  ot1stg  6152  ot2ndg  6153  eloprabi  6196  1stconst  6221  algrflemg  6230  tfrlem1  6308  tfrlem3ag  6309  tfrlem3a  6310  tfrlem9  6319  tfr0dm  6322  tfrlemisucaccv  6325  tfrlemiubacc  6330  tfrlemiex  6331  tfrlemi1  6332  tfr1onlem3ag  6337  tfr1onlemsucaccv  6341  tfr1onlemubacc  6346  tfr1onlemex  6347  tfr1onlemaccex  6348  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllemubacc  6359  tfrcllemex  6360  tfrcllemaccex  6361  tfrcllemres  6362  tfrcldm  6363  rdgivallem  6381  rdgival  6382  rdgss  6383  rdgisuc1  6384  rdgon  6386  rdg0  6387  frec0g  6397  frecabcl  6399  freccllem  6402  frecfcllem  6404  frecsuclem  6406  frecsuc  6407  frecrdg  6408  oav2  6463  omv2  6465  xpdom2  6830  xpmapenlem  6848  xpmapen  6849  ac6sfi  6897  1stinl  7072  2ndinl  7073  1stinr  7074  2ndinr  7075  updjudhcoinlf  7078  updjudhcoinrg  7079  caseinl  7089  caseinr  7090  omp1eomlem  7092  omp1eom  7093  difinfsn  7098  ctmlemr  7106  ctm  7107  ctssdclemn0  7108  ctssdccl  7109  nnnninfeq  7125  nnnninfeq2  7126  enomnilem  7135  enmkvlem  7158  enwomnilem  7166  exmidfodomrlemeldju  7197  exmidfodomrlemreseldju  7198  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidaclem  7206  cc2  7265  cc3  7266  ltdfpr  7504  genpelvl  7510  genpelvu  7511  recexpr  7636  cauappcvgprlem1  7657  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem1  7677  caucvgprlem2  7678  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkeqj  7688  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlem1  7707  caucvgprprlem2  7708  caucvgsr  7800  axcaucvglemval  7895  axcaucvglemres  7897  fv0p1e1  9032  uzin  9558  cnref1o  9648  fzsuc2  10076  fseq1m1p1  10092  fzoss2  10169  elfzonlteqm1  10207  divfl0  10293  flqzadd  10295  fldiv4p1lem1div2  10302  ceilqval  10303  flqdiv  10318  modqval  10321  modqfrac  10334  modqmulnn  10339  modqid  10346  modqcyc  10356  modqdi  10389  frec2uzuzd  10399  frec2uzrdg  10406  frecuzrdgrcl  10407  frecuzrdgtcl  10409  frecuzrdgsuc  10411  frecuzrdgrclt  10412  frecuzrdgg  10413  frecuzrdgfunlem  10416  frecuzrdgsuctlem  10420  iseqovex  10453  iseqvalcbv  10454  seq3val  10455  seqvalcd  10456  seq3m1  10465  seq3shft2  10470  monoord  10473  monoord2  10474  iseqf1olemqval  10484  iseqf1olemab  10486  iseqf1olemqk  10491  iseqf1olemjpcl  10492  iseqf1olemqpcl  10493  iseqf1olemfvp  10494  seq3f1olemqsumkj  10495  seq3f1olemqsumk  10496  seq3f1olemqsum  10497  seq3f1olemp  10499  seq3f1oleml  10500  seq3homo  10507  exp3val  10519  expnegap0  10525  facnn2  10709  facwordi  10715  faclbnd6  10719  bcval  10724  bccmpl  10729  bcn0  10730  bcm1k  10735  bcp1n  10736  bcn2  10739  hashinfom  10753  hashennn  10755  hashsng  10773  omgadd  10777  hashprg  10783  fihashssdif  10793  hashdifpr  10795  hashfzo  10797  hashfzp1  10799  hashxp  10801  zfz1isolemiso  10814  zfz1iso  10816  shftval2  10830  shftval3  10831  shftval4  10832  shftval5  10833  seq3shft  10842  imval  10854  imre  10855  reim  10856  crim  10862  reim0  10865  mulreap  10868  recj  10871  reneg  10872  readd  10873  resub  10874  remullem  10875  redivap  10878  imcj  10879  imneg  10880  imadd  10881  imsub  10882  imdivap  10885  cjsub  10896  cjexp  10897  cjreim2  10908  cjap  10910  cjdivap  10913  cnrecnv  10914  cvg1nlemcau  10988  cvg1nlemres  10989  absval  11005  rennim  11006  sqrtdiv  11046  sqrtmsq  11049  absneg  11054  abscj  11056  absval2  11061  absreim  11072  absmul  11073  absdivap  11074  absid  11075  absre  11081  absexp  11083  absexpzap  11084  absimle  11088  abssub  11105  abs3dif  11109  abs2dif  11110  abs2dif2  11111  recan  11113  cau3lem  11118  max0addsup  11223  minabs  11239  bdtrilem  11242  clim  11284  clim2  11286  clim0  11288  clim0c  11289  climi0  11292  climconst  11293  climshftlemg  11305  climcn1  11311  climcn2  11312  addcn2  11313  subcn2  11314  mulcn2  11315  reccn2ap  11316  cjcn2  11319  recn2  11320  imcn2  11321  iser3shft  11349  climcau  11350  climcvg1nlem  11352  climcvg1n  11353  serf0  11355  summodclem3  11383  summodclem2a  11384  summodc  11386  fsumf1o  11393  sumsnf  11412  fsumm1  11419  fsumcnv  11440  fsumabs  11468  fsumrelem  11474  iserabs  11478  hash2iun1dif1  11483  isumshft  11493  isumsplit  11494  expcnvap0  11505  expcnv  11507  cvgratnnlemseq  11529  cvgratnnlemrate  11533  cvgratz  11535  mertenslemub  11537  mertenslemi1  11538  mertenslem2  11539  mertensabs  11540  prodmodclem3  11578  fprodf1o  11591  prodsnf  11595  fprodm1  11601  fprodabs  11619  fprodcnv  11628  efcllemp  11661  efcj  11676  efaddlem  11677  efcan  11679  efsub  11684  efexp  11685  efzval  11686  efgt0  11687  eftlub  11693  efltim  11701  sinval  11705  cosval  11706  tanval3ap  11717  resinval  11718  recosval  11719  resin4p  11721  recos4p  11722  sinneg  11729  cosneg  11730  efmival  11736  efeul  11737  sinadd  11739  cosadd  11740  sinsub  11743  cossub  11744  addsin  11745  subsin  11746  addcos  11749  subcos  11750  sincossq  11751  sin2t  11752  cos2t  11753  sin01bnd  11760  cos01bnd  11761  sin02gt0  11766  cos12dec  11770  absefi  11771  absef  11772  absefib  11773  efieq1re  11774  demoivre  11775  demoivreALT  11776  flodddiv4  11933  alginv  12041  algcvg  12042  eucalgval  12048  eucalginv  12050  eucalglt  12051  eucalgcvga  12052  eucalg  12053  lcmgcd  12072  lcm1  12075  sqpweven  12169  2sqpwodd  12170  sqne2sq  12171  qnumval  12179  qdenval  12180  qden1elz  12199  nn0sqrtelqelz  12200  phival  12207  dfphi2  12214  phiprmpw  12216  phiprm  12217  eulerthlemth  12226  hashgcdeq  12233  phisum  12234  pythagtriplem6  12264  pythagtriplem7  12265  pythagtriplem12  12269  pythagtriplem14  12271  fldivp1  12340  ennnfonelemg  12398  ennnfonelemp1  12401  ennnfonelemkh  12407  ennnfonelemhf1o  12408  ennnfonelemnn0  12417  ctinfomlemom  12422  ctiunctlemu1st  12429  ctiunctlemu2nd  12430  ctiunctlemudc  12432  ctiunctlemfo  12434  isstruct2im  12466  isstruct2r  12467  strslfv3  12502  setsslid  12507  ressbasd  12521  resseqnbasd  12526  ressplusgd  12581  imasex  12708  imasival  12709  f1ocpbl  12714  f1ovscpbl  12715  imasaddvallemg  12718  ismhm  12807  mhmpropd  12811  mhmlin  12812  mhmf1o  12815  mhmco  12828  grpinvsub  12906  mhmlem  12932  mhmid  12933  mhmmnd  12934  ghmgrp  12936  mulgfvalg  12939  mulgval  12940  mulgnegnn  12947  mulgneg  12955  mulgnegneg  12956  mulgm1  12957  mulginvcom  12961  mulgz  12964  mulgnndir  12965  mulgdir  12968  mulgass  12973  mhmmulg  12977  subgmulg  13001  isnsg  13015  eqgfval  13034  ablsub2inv  13067  mgpplusgg  13087  mgpbasg  13089  mgpscag  13090  mgptsetg  13091  mgpdsg  13093  isring  13136  ringm2neg  13185  opprmulfvalg  13195  opprsllem  13199  isunitd  13228  opprunitd  13232  invrfvald  13244  rdivmuldivd  13266  istps  13423  tpspropd  13427  eltpsg  13431  txvalex  13647  txval  13648  txbasval  13660  upxp  13665  uptx  13667  txrest  13669  cnmpt11  13676  cnmpt21  13684  hmeontr  13706  txhmeo  13712  psmetxrge0  13725  xmetunirn  13751  mopnval  13835  mopntopon  13836  isxms  13844  isxms2  13845  isms  13846  msrtri  13869  xmspropd  13870  mspropd  13871  setsmsbasg  13872  setsmsdsg  13873  setsmstsetg  13874  comet  13892  metcnpi  13908  metcnpi2  13909  cnbl0  13927  cnblcld  13928  resubmet  13941  elcncf  13953  cncfi  13958  rescncf  13961  mulc1cncf  13969  cncfco  13971  cncfmptid  13976  addccncf  13979  cdivcncfap  13980  negcncf  13981  mulcncflem  13983  ivthinclemlopn  14007  ivthinclemuopn  14009  limccl  14021  ellimc3apf  14022  limcimolemlt  14026  cnplimclemle  14030  limccnpcntop  14037  reldvg  14041  dvfvalap  14043  dveflem  14080  dvef  14081  sin0pilem1  14095  ef2kpi  14120  sinperlem  14122  sin2kpi  14125  cos2kpi  14126  sin2pim  14127  cos2pim  14128  ptolemy  14138  sincosq2sgn  14141  sincosq3sgn  14142  sincosq4sgn  14143  sinq12gt0  14144  tangtx  14152  sincosq1eq  14153  abssinper  14160  sinkpi  14161  coskpi  14162  cosq34lt1  14164  relogeftb  14179  relogoprlem  14182  relogexp  14186  rpcxpef  14208  logcxp  14211  1cxp  14214  ecxp  14215  rpcxpadd  14219  rpmulcxp  14223  cxpmul  14226  abscxp  14228  logsqrt  14236  rpabscxpbnd  14252  rpcxplogb  14275  lgsval  14298  lgsval2lem  14304  lgsval4a  14316  lgsdi  14331  nnsf  14636  peano4nninf  14637  peano3nninf  14638  nninfalllem1  14639  nninfall  14640  nninfsellemdc  14641  nninfsellemeq  14645  nninfsellemqall  14646  nninfsellemeqinf  14647  nninfsel  14648  exmidsbthr  14653  qdencn  14657  refeq  14658  isomninnlem  14660  apdifflemr  14677  apdiff  14678  ismkvnnlem  14682  nconstwlpolem  14694