Theorem fveqeq2 5707

Description: Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.)

Assertion

Ref	Expression
fveqeq2	⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

Proof of Theorem fveqeq2

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	fveqeq2d 5706	1 ⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402  ‘cfv 5380

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 4132  df-iota 5340  df-fv 5388

This theorem is used by:  uchoice  6375  suppfnss  6501  suppssfvg  6507  2omap  7324  nninfninc  7469  nnnninfeq2  7475  fodjum  7492  fodju0  7493  fodjuomnilemres  7494  fodjumkvlemres  7505  fodjumkv  7506  enmkvlem  7507  enwomnilem  7515  nninfwlporlemd  7518  nninfwlpoimlemginf  7522  nninfwlpoim  7525  nninfinfwlpo  7526  seq3id3  10981  seq3id2  10983  seq3z  10985  hashfibclem  11303  hashfibc  11304  wrdmap  11357  wrdl1s1  11419  wrdind  11515  wrd2ind  11516  reuccatpfxs1lem  11539  reuccatpfxs1  11540  fsum3cvg  12169  summodclem2a  12172  fproddccvg  12363  nninfctlemfo  12841  algfx  12854  ballotfilemelo  13279  ballotfilemfmpn  13291  ballotfilemiex  13301  ballotfilemi1  13302  ballotfilemii  13303  ballotfilemscl  13304  ballotfilemimin  13306  ballotfilemfrcn0  13330  ballotfilemirc  13332  ballotfi  13339  ennnfonelemim  13372  ghmf1  14134  gsumresfi  14262  ivthreinc  15888  ivthdich  15896  reeff1oleme  16015  sin0pilem2  16026  lgsquadlem1  16418  gropd  16510  grstructd2dom  16511  uhgr2edg  16669  usgredg2v  16687  ushgredgedgloop  16691  vtxlpfi  16753  vtxdumgrfival  16761  isclwwlkng  16869  clwwlkn1loopb  16883  s2elclwwlknon2  16899  bj-charfunbi  17059  pw1map  17247  nninfomnilem  17284  nnnninfex  17288  trilpolemlt1  17314  redcwlpolemeq1  17328  nconstwlpolem0  17337  nconstwlpolem  17339  neapmkvlem  17341