Theorem fveqeq2 5648

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 5647	1 ⊢ (𝐴 = 𝐵 → ((𝐹‘𝐴) = 𝐶 ↔ (𝐹‘𝐵) = 𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  ‘cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334

This theorem is referenced by:  uchoice  6300  nninfninc  7322  nnnninfeq2  7328  fodjum  7345  fodju0  7346  fodjuomnilemres  7347  fodjumkvlemres  7358  fodjumkv  7359  enmkvlem  7360  enwomnilem  7368  nninfwlporlemd  7371  nninfwlpoimlemginf  7375  nninfwlpoim  7378  nninfinfwlpo  7379  seq3id3  10787  seq3id2  10789  seq3z  10791  wrdmap  11149  wrdl1s1  11211  wrdind  11307  wrd2ind  11308  reuccatpfxs1lem  11331  reuccatpfxs1  11332  fsum3cvg  11957  summodclem2a  11960  fproddccvg  12151  nninfctlemfo  12629  algfx  12642  ennnfonelemim  13063  gsumfzz  13596  ghmf1  13878  mplsubgfilemcl  14732  ivthreinc  15388  ivthdich  15396  reeff1oleme  15515  sin0pilem2  15525  lgsquadlem1  15825  gropd  15917  grstructd2dom  15918  uhgr2edg  16076  usgredg2v  16094  ushgredgedgloop  16098  vtxlpfi  16160  vtxdumgrfival  16168  isclwwlkng  16276  clwwlkn1loopb  16290  s2elclwwlknon2  16306  bj-charfunbi  16457  2omap  16645  pw1map  16647  nninfomnilem  16671  nnnninfex  16675  trilpolemlt1  16696  redcwlpolemeq1  16710  nconstwlpolem0  16719  nconstwlpolem  16721  neapmkvlem  16723