Theorem fveq2i 5378

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

Hypothesis

Ref	Expression
fveq2i.1	|- A = B

Assertion

Ref	Expression
fveq2i	|- ( F ` A ) = ( F ` B )

Proof of Theorem fveq2i

Step	Hyp	Ref	Expression
1		fveq2i.1	. 2 |- A = B
2		fveq2 5375	. 2 |- ( A = B -> ( F ` A ) = ( F ` B ) )
3	1, 2	ax-mp 7	1 |- ( F ` A ) = ( F ` B )

Syntax hints:   = wceq 1314   ` cfv 5081

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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-rex 2396  df-v 2659  df-un 3041  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-br 3896  df-iota 5046  df-fv 5089

This theorem is referenced by:  fveq12i  5381  ot1stg  6004  ot2ndg  6005  ot3rdgg  6006  algrflem  6080  tfr2a  6172  tfr0dm  6173  tfr0  6174  infisoti  6871  1prl  7311  1pru  7312  ltexprlemell  7354  ltexprlemelu  7355  recexprlemell  7378  recexprlemelu  7379  cauappcvgprlemm  7401  cauappcvgprlemopl  7402  cauappcvgprlemlol  7403  cauappcvgprlemopu  7404  cauappcvgprlemupu  7405  cauappcvgprlemdisj  7407  cauappcvgprlemloc  7408  cauappcvgprlemladdfu  7410  cauappcvgprlemladdfl  7411  cauappcvgprlemladdru  7412  cauappcvgprlem2  7416  caucvgprlemm  7424  caucvgprlemopl  7425  caucvgprlemlol  7426  caucvgprlemopu  7427  caucvgprlemupu  7428  caucvgprlemdisj  7430  caucvgprlemloc  7431  caucvgprlemladdfu  7433  caucvgprlem2  7436  caucvgprprlemell  7441  caucvgprprlemelu  7442  caucvgprprlemml  7450  caucvgprprlemmu  7451  caucvgprprlemexbt  7462  caucvgprprlem2  7466  caucvgsr  7544  axcaucvg  7635  infrenegsupex  9291  fseq1p1m1  9767  rebtwn2zlemstep  9923  rebtwn2z  9925  fldiv4p1lem1div2  9971  frec2uzsucd  10067  frec2uzrdg  10075  frecuzrdgsuc  10080  frecuzrdgg  10082  frecuzrdgsuctlem  10089  frecfzennn  10092  0tonninf  10105  1tonninf  10106  seq3val  10124  seqvalcd  10125  facp1  10369  fac2  10370  fac3  10371  fac4  10372  4bc2eq6  10413  fihasheq0  10433  hashprg  10447  hashp1i  10449  pr0hash2ex  10454  hashfzo  10461  hashxp  10465  zfz1isolemsplit  10474  rei  10564  imi  10565  sqrt1  10710  sqrt4  10711  sqrt9  10712  abs0  10722  absi  10723  infxrnegsupex  10924  fsumabs  11126  fsumrelem  11132  hashrabrex  11142  hashuni  11143  isumnn0nn  11154  mertenslem2  11197  ege2le3  11228  efsep  11248  efgt1p2  11252  efgt1p  11253  sin0  11287  cos0  11288  ef01bndlem  11314  cos2bnd  11318  sin4lt0  11324  eucalg  11586  prmind2  11647  dfphi2  11741  phiprmpw  11743  phimullem  11746  ennnfonelemjn  11760  ennnfonelem1  11765  ennnfonelemhf1o  11771  sn0cld  12149  txval  12266  comet  12488  cnmetdval  12518  ex-ceil  12631  ex-fac  12633  nninfsellemqall  12901  nninfomni  12905  nninffeq  12906  isomninnlem  12915