Theorem fveqeq2 5563

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364  ‘cfv 5254

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262

This theorem is referenced by:  uchoice  6190  nninfninc  7182  nnnninfeq2  7188  fodjum  7205  fodju0  7206  fodjuomnilemres  7207  fodjumkvlemres  7218  fodjumkv  7219  enmkvlem  7220  enwomnilem  7228  nninfwlporlemd  7231  nninfwlpoimlemginf  7235  nninfwlpoim  7237  seq3id3  10595  seq3id2  10597  seq3z  10599  wrdmap  10945  fsum3cvg  11521  summodclem2a  11524  fproddccvg  11715  nninfctlemfo  12177  algfx  12190  ennnfonelemim  12581  gsumfzz  13067  ghmf1  13343  ivthreinc  14799  ivthdich  14807  reeff1oleme  14907  sin0pilem2  14917  lgsquadlem1  15191  bj-charfunbi  15303  nninfomnilem  15508  trilpolemlt1  15531  redcwlpolemeq1  15544  nconstwlpolem0  15553  nconstwlpolem  15555  neapmkvlem  15557