Theorem fveq2i 5592

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

Syntax hints:   = wceq 1373  ‘cfv 5280

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-iota 5241  df-fv 5288

This theorem is referenced by:  fveq12i  5595  ot1stg  6251  ot2ndg  6252  ot3rdgg  6253  algrflem  6328  tfr2a  6420  tfr0dm  6421  tfr0  6422  infisoti  7149  1prl  7688  1pru  7689  ltexprlemell  7731  ltexprlemelu  7732  recexprlemell  7755  recexprlemelu  7756  cauappcvgprlemm  7778  cauappcvgprlemopl  7779  cauappcvgprlemlol  7780  cauappcvgprlemopu  7781  cauappcvgprlemupu  7782  cauappcvgprlemdisj  7784  cauappcvgprlemloc  7785  cauappcvgprlemladdfu  7787  cauappcvgprlemladdfl  7788  cauappcvgprlemladdru  7789  cauappcvgprlem2  7793  caucvgprlemm  7801  caucvgprlemopl  7802  caucvgprlemlol  7803  caucvgprlemopu  7804  caucvgprlemupu  7805  caucvgprlemdisj  7807  caucvgprlemloc  7808  caucvgprlemladdfu  7810  caucvgprlem2  7813  caucvgprprlemell  7818  caucvgprprlemelu  7819  caucvgprprlemml  7827  caucvgprprlemmu  7828  caucvgprprlemexbt  7839  caucvgprprlem2  7843  suplocexprlem2b  7847  suplocexprlemlub  7857  caucvgsr  7935  axcaucvg  8033  infrenegsupex  9735  fseq1p1m1  10236  fz0to4untppr  10266  rebtwn2zlemstep  10417  rebtwn2z  10419  fldiv4p1lem1div2  10470  frec2uzsucd  10568  frec2uzrdg  10576  frecuzrdgsuc  10581  frecuzrdgg  10583  frecuzrdgsuctlem  10590  frecfzennn  10593  0tonninf  10607  1tonninf  10608  seq3val  10627  seqvalcd  10628  seqf1oglem2  10687  facp1  10897  fac2  10898  fac3  10899  fac4  10900  4bc2eq6  10941  fihasheq0  10960  hashprg  10975  hashp1i  10977  pr0hash2ex  10982  hashfzo  10989  hashxp  10993  zfz1isolemsplit  11005  rei  11285  imi  11286  sqrt1  11432  sqrt4  11433  sqrt9  11434  abs0  11444  absi  11445  infxrnegsupex  11649  fsumabs  11851  fsumrelem  11857  hashrabrex  11867  hashuni  11868  isumnn0nn  11879  mertenslem2  11922  ege2le3  12057  efsep  12077  efgt1p2  12081  efgt1p  12082  sin0  12115  cos0  12116  ef01bndlem  12142  cos2bnd  12146  sin4lt0  12153  m1bits  12346  nninfctlemfo  12436  eucalg  12456  prmind2  12517  dfphi2  12617  phiprmpw  12619  phimullem  12622  pockthlem  12754  pockthg  12755  prmunb  12760  ennnfonelemjn  12848  ennnfonelem1  12853  ennnfonelemhf1o  12859  imasplusg  13215  ringidvalg  13798  rmodislmod  14188  lspprid2  14249  sn0cld  14684  txval  14802  hmeontr  14860  comet  15046  cnmetdval  15076  sinhalfpilem  15338  cospi  15347  sincos4thpi  15387  sincos6thpi  15389  sincos3rdpi  15390  sinkpi  15394  reeflog  15410  logbleb  15508  logblt  15509  sqrt2cxp2logb9e3  15522  lgsval2lem  15562  lgsquadlem2  15630  ex-ceil  15801  ex-fac  15803  012of  16069  2o01f  16070  nninfsellemqall  16093  nninfomni  16097  nninffeq  16098  isomninnlem  16110  iswomninnlem  16129  ismkvnnlem  16132