Theorem fveq2i 5499

Description: Equality inference for function value. (Contributed by NM, 28-Jul-1999.)

Hypothesis

Ref	Expression
fveq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
fveq2i	⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Proof of Theorem fveq2i

Step	Hyp	Ref	Expression
1		fveq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		fveq2 5496	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Syntax hints:   = wceq 1348  ‘cfv 5198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206

This theorem is referenced by:  fveq12i  5502  ot1stg  6131  ot2ndg  6132  ot3rdgg  6133  algrflem  6208  tfr2a  6300  tfr0dm  6301  tfr0  6302  infisoti  7009  1prl  7517  1pru  7518  ltexprlemell  7560  ltexprlemelu  7561  recexprlemell  7584  recexprlemelu  7585  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemopu  7610  cauappcvgprlemupu  7611  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  cauappcvgprlem2  7622  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemopu  7633  caucvgprlemupu  7634  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprlem2  7642  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemexbt  7668  caucvgprprlem2  7672  suplocexprlem2b  7676  suplocexprlemlub  7686  caucvgsr  7764  axcaucvg  7862  infrenegsupex  9553  fseq1p1m1  10050  fz0to4untppr  10080  rebtwn2zlemstep  10209  rebtwn2z  10211  fldiv4p1lem1div2  10261  frec2uzsucd  10357  frec2uzrdg  10365  frecuzrdgsuc  10370  frecuzrdgg  10372  frecuzrdgsuctlem  10379  frecfzennn  10382  0tonninf  10395  1tonninf  10396  seq3val  10414  seqvalcd  10415  facp1  10664  fac2  10665  fac3  10666  fac4  10667  4bc2eq6  10708  fihasheq0  10728  hashprg  10743  hashp1i  10745  pr0hash2ex  10750  hashfzo  10757  hashxp  10761  zfz1isolemsplit  10773  rei  10863  imi  10864  sqrt1  11010  sqrt4  11011  sqrt9  11012  abs0  11022  absi  11023  infxrnegsupex  11226  fsumabs  11428  fsumrelem  11434  hashrabrex  11444  hashuni  11445  isumnn0nn  11456  mertenslem2  11499  ege2le3  11634  efsep  11654  efgt1p2  11658  efgt1p  11659  sin0  11692  cos0  11693  ef01bndlem  11719  cos2bnd  11723  sin4lt0  11729  eucalg  12013  prmind2  12074  dfphi2  12174  phiprmpw  12176  phimullem  12179  pockthlem  12308  pockthg  12309  prmunb  12314  ennnfonelemjn  12357  ennnfonelem1  12362  ennnfonelemhf1o  12368  sn0cld  12931  txval  13049  hmeontr  13107  comet  13293  cnmetdval  13323  sinhalfpilem  13506  cospi  13515  sincos4thpi  13555  sincos6thpi  13557  sincos3rdpi  13558  sinkpi  13562  reeflog  13578  logbleb  13673  logblt  13674  sqrt2cxp2logb9e3  13687  lgsval2lem  13705  ex-ceil  13761  ex-fac  13763  012of  14028  2o01f  14029  nninfsellemqall  14048  nninfomni  14052  nninffeq  14053  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084