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  10982  seq3id2  10984  seq3z  10986  hashfibclem  11304  hashfibc  11305  wrdmap  11358  wrdl1s1  11420  wrdind  11516  wrd2ind  11517  reuccatpfxs1lem  11540  reuccatpfxs1  11541  fsum3cvg  12170  summodclem2a  12173  fproddccvg  12364  nninfctlemfo  12842  algfx  12855  ballotfilemelo  13280  ballotfilemfmpn  13292  ballotfilemiex  13302  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemscl  13305  ballotfilemimin  13307  ballotfilemfrcn0  13331  ballotfilemirc  13333  ballotfi  13340  ennnfonelemim  13373  ghmf1  14135  gsumresfi  14263  mplsubgfilemcl  15215  ivthreinc  15871  ivthdich  15879  reeff1oleme  15998  sin0pilem2  16009  lgsquadlem1  16401  gropd  16493  grstructd2dom  16494  uhgr2edg  16652  usgredg2v  16670  ushgredgedgloop  16674  vtxlpfi  16736  vtxdumgrfival  16744  isclwwlkng  16852  clwwlkn1loopb  16866  s2elclwwlknon2  16882  bj-charfunbi  17042  pw1map  17230  nninfomnilem  17267  nnnninfex  17271  trilpolemlt1  17297  redcwlpolemeq1  17311  nconstwlpolem0  17320  nconstwlpolem  17322  neapmkvlem  17324