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  6299  nninfninc  7321  nnnninfeq2  7327  fodjum  7344  fodju0  7345  fodjuomnilemres  7346  fodjumkvlemres  7357  fodjumkv  7358  enmkvlem  7359  enwomnilem  7367  nninfwlporlemd  7370  nninfwlpoimlemginf  7374  nninfwlpoim  7377  nninfinfwlpo  7378  seq3id3  10785  seq3id2  10787  seq3z  10789  wrdmap  11144  wrdl1s1  11206  wrdind  11302  wrd2ind  11303  reuccatpfxs1lem  11326  reuccatpfxs1  11327  fsum3cvg  11938  summodclem2a  11941  fproddccvg  12132  nninfctlemfo  12610  algfx  12623  ennnfonelemim  13044  gsumfzz  13577  ghmf1  13859  mplsubgfilemcl  14712  ivthreinc  15368  ivthdich  15376  reeff1oleme  15495  sin0pilem2  15505  lgsquadlem1  15805  gropd  15897  grstructd2dom  15898  uhgr2edg  16056  usgredg2v  16074  ushgredgedgloop  16078  vtxlpfi  16140  vtxdumgrfival  16148  isclwwlkng  16256  clwwlkn1loopb  16270  s2elclwwlknon2  16286  bj-charfunbi  16406  2omap  16594  pw1map  16596  nninfomnilem  16620  nnnninfex  16624  trilpolemlt1  16645  redcwlpolemeq1  16658  nconstwlpolem0  16667  nconstwlpolem  16669  neapmkvlem  16671