Theorem fveq2i 5424

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 5421	. 2 |- ( A = B -> ( F ` A ) = ( F ` B ) )
3	1, 2	ax-mp 5	1 |- ( F ` A ) = ( F ` B )

Syntax hints:   = wceq 1331   ` cfv 5123

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131

This theorem is referenced by:  fveq12i  5427  ot1stg  6050  ot2ndg  6051  ot3rdgg  6052  algrflem  6126  tfr2a  6218  tfr0dm  6219  tfr0  6220  infisoti  6919  1prl  7363  1pru  7364  ltexprlemell  7406  ltexprlemelu  7407  recexprlemell  7430  recexprlemelu  7431  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemopu  7456  cauappcvgprlemupu  7457  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  cauappcvgprlem2  7468  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemopu  7479  caucvgprlemupu  7480  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprlem2  7488  caucvgprprlemell  7493  caucvgprprlemelu  7494  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemexbt  7514  caucvgprprlem2  7518  suplocexprlem2b  7522  suplocexprlemlub  7532  caucvgsr  7610  axcaucvg  7708  infrenegsupex  9389  fseq1p1m1  9874  rebtwn2zlemstep  10030  rebtwn2z  10032  fldiv4p1lem1div2  10078  frec2uzsucd  10174  frec2uzrdg  10182  frecuzrdgsuc  10187  frecuzrdgg  10189  frecuzrdgsuctlem  10196  frecfzennn  10199  0tonninf  10212  1tonninf  10213  seq3val  10231  seqvalcd  10232  facp1  10476  fac2  10477  fac3  10478  fac4  10479  4bc2eq6  10520  fihasheq0  10540  hashprg  10554  hashp1i  10556  pr0hash2ex  10561  hashfzo  10568  hashxp  10572  zfz1isolemsplit  10581  rei  10671  imi  10672  sqrt1  10818  sqrt4  10819  sqrt9  10820  abs0  10830  absi  10831  infxrnegsupex  11032  fsumabs  11234  fsumrelem  11240  hashrabrex  11250  hashuni  11251  isumnn0nn  11262  mertenslem2  11305  ege2le3  11377  efsep  11397  efgt1p2  11401  efgt1p  11402  sin0  11436  cos0  11437  ef01bndlem  11463  cos2bnd  11467  sin4lt0  11473  eucalg  11740  prmind2  11801  dfphi2  11896  phiprmpw  11898  phimullem  11901  ennnfonelemjn  11915  ennnfonelem1  11920  ennnfonelemhf1o  11926  sn0cld  12306  txval  12424  hmeontr  12482  comet  12668  cnmetdval  12698  sinhalfpilem  12872  cospi  12881  sincos4thpi  12921  sincos6thpi  12923  sincos3rdpi  12924  sinkpi  12928  ex-ceil  12938  ex-fac  12940  nninfsellemqall  13211  nninfomni  13215  nninffeq  13216  isomninnlem  13225