Theorem fveq2i 5698

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

This proof depends on syntax axioms:   = wceq 1402  ‘cfv 5377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385

This theorem is used by:  fveq12i  5701  ot1stg  6386  ot2ndg  6387  ot3rdgg  6388  algrflem  6465  tfr2a  6592  tfr0dm  6593  tfr0  6594  infisoti  7373  1prl  7923  1pru  7924  ltexprlemell  7966  ltexprlemelu  7967  recexprlemell  7990  recexprlemelu  7991  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlem2  8028  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprlem2  8048  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemexbt  8074  caucvgprprlem2  8078  suplocexprlem2b  8082  suplocexprlemlub  8092  caucvgsr  8170  axcaucvg  8268  infrenegsupex  10004  fseq1p1m1  10512  fz0to4untppr  10542  rebtwn2zlemstep  10698  rebtwn2z  10700  fldiv4p1lem1div2  10755  frec2uzsucd  10853  frec2uzrdg  10861  frecuzrdgsuc  10866  frecuzrdgg  10868  frecuzrdgsuctlem  10875  frecfzennn  10878  0tonninf  10892  1tonninf  10893  seq3val  10912  seqvalcd  10913  seqf1oglem2  10972  facp1  11184  fac2  11185  fac3  11186  fac4  11187  4bc2eq6  11229  fihasheq0  11248  hashprg  11265  hashp1i  11267  pr0hash2ex  11272  hashfzo  11279  hashxp  11283  hashfibc  11299  hashf1lem2  11302  zfz1isolemsplit  11306  hashtpgim  11313  hashtpg  11315  cats1lend  11555  rei  11681  imi  11682  sqrt1  11828  sqrt4  11829  sqrt9  11830  abs0  11840  absi  11841  infxrnegsupex  12048  fsumabs  12251  fsumrelem  12257  hashrabrex  12267  hashuni  12268  isumnn0nn  12279  mertenslem2  12322  ege2le3  12457  efsep  12477  efgt1p2  12481  efgt1p  12482  sin0  12515  cos0  12516  ef01bndlem  12542  cos2bnd  12546  sin4lt0  12553  m1bits  12746  nninfctlemfo  12836  eucalg  12856  prmind2  12917  dfphi2  13021  phiprmpw  13023  phimullem  13026  pockthlem  13158  pockthg  13159  prmunb  13164  ballotfilem1  13272  ballotfilem2  13280  ballotfilemfval0  13287  ballotfilem4  13293  ballotfilemi1  13297  ballotfilemii  13298  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemgun  13320  ballotfilemth  13333  ennnfonelemjn  13345  ennnfonelem1  13350  ennnfonelemhf1o  13356  imasplusg  13682  gsump1  14241  ringidvalg  14348  rmodislmod  14772  lspprid2  14833  isassa  15086  assamulgscmlem2  15126  sn0cld  15329  txval  15447  hmeontr  15505  comet  15691  cnmetdval  15721  sinhalfpilem  15984  cospi  15993  sincos4thpi  16033  sincos6thpi  16035  sincos3rdpi  16036  sinkpi  16040  reeflog  16056  logfac  16090  logbleb  16158  logblt  16159  sqrt2cxp2logb9e3  16172  birthdaylem2  16187  ppiprm  16220  ppinprm  16221  chtprm  16222  chtnprm  16223  ppi1  16231  ppi1i  16233  ppi2i  16234  cht2  16237  cht3  16238  ppiqub  16254  chtqub  16257  bposlem6  16277  bposlem8  16279  bposlem9  16280  lgsval2lem  16295  lgsquadlem2  16363  setsiedg  16459  wlkres  16786  trlreslem  16796  clwwlkccatlem  16807  eupthvdres  16882  eupth2lem3fi  16883  konigsbergvtx  16889  konigsbergiedg  16890  konigsberglem5  16899  konigsberg  16900  ex-ceil  16906  ex-fac  16908  012of  17189  2o01f  17190  nninfsellemqall  17224  nninfomni  17228  nninffeq  17229  isomninnlem  17245  iswomninnlem  17266  ismkvnnlem  17269