Theorem fveq2i 5520

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 5517	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Syntax hints:   = wceq 1353  ‘cfv 5218

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 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226

This theorem is referenced by:  fveq12i  5523  ot1stg  6155  ot2ndg  6156  ot3rdgg  6157  algrflem  6232  tfr2a  6324  tfr0dm  6325  tfr0  6326  infisoti  7033  1prl  7556  1pru  7557  ltexprlemell  7599  ltexprlemelu  7600  recexprlemell  7623  recexprlemelu  7624  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemopu  7649  cauappcvgprlemupu  7650  cauappcvgprlemdisj  7652  cauappcvgprlemloc  7653  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  cauappcvgprlemladdru  7657  cauappcvgprlem2  7661  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemopu  7672  caucvgprlemupu  7673  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemladdfu  7678  caucvgprlem2  7681  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemexbt  7707  caucvgprprlem2  7711  suplocexprlem2b  7715  suplocexprlemlub  7725  caucvgsr  7803  axcaucvg  7901  infrenegsupex  9596  fseq1p1m1  10096  fz0to4untppr  10126  rebtwn2zlemstep  10255  rebtwn2z  10257  fldiv4p1lem1div2  10307  frec2uzsucd  10403  frec2uzrdg  10411  frecuzrdgsuc  10416  frecuzrdgg  10418  frecuzrdgsuctlem  10425  frecfzennn  10428  0tonninf  10441  1tonninf  10442  seq3val  10460  seqvalcd  10461  facp1  10712  fac2  10713  fac3  10714  fac4  10715  4bc2eq6  10756  fihasheq0  10775  hashprg  10790  hashp1i  10792  pr0hash2ex  10797  hashfzo  10804  hashxp  10808  zfz1isolemsplit  10820  rei  10910  imi  10911  sqrt1  11057  sqrt4  11058  sqrt9  11059  abs0  11069  absi  11070  infxrnegsupex  11273  fsumabs  11475  fsumrelem  11481  hashrabrex  11491  hashuni  11492  isumnn0nn  11503  mertenslem2  11546  ege2le3  11681  efsep  11701  efgt1p2  11705  efgt1p  11706  sin0  11739  cos0  11740  ef01bndlem  11766  cos2bnd  11770  sin4lt0  11776  eucalg  12061  prmind2  12122  dfphi2  12222  phiprmpw  12224  phimullem  12227  pockthlem  12356  pockthg  12357  prmunb  12362  ennnfonelemjn  12405  ennnfonelem1  12410  ennnfonelemhf1o  12416  imasplusg  12734  ringidvalg  13149  rmodislmod  13446  sn0cld  13676  txval  13794  hmeontr  13852  comet  14038  cnmetdval  14068  sinhalfpilem  14251  cospi  14260  sincos4thpi  14300  sincos6thpi  14302  sincos3rdpi  14303  sinkpi  14307  reeflog  14323  logbleb  14418  logblt  14419  sqrt2cxp2logb9e3  14432  lgsval2lem  14450  ex-ceil  14517  ex-fac  14519  012of  14784  2o01f  14785  nninfsellemqall  14803  nninfomni  14807  nninffeq  14808  isomninnlem  14817  iswomninnlem  14836  ismkvnnlem  14839