Theorem fveqeq2 5564

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

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

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 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263

This theorem is referenced by:  uchoice  6192  nninfninc  7184  nnnninfeq2  7190  fodjum  7207  fodju0  7208  fodjuomnilemres  7209  fodjumkvlemres  7220  fodjumkv  7221  enmkvlem  7222  enwomnilem  7230  nninfwlporlemd  7233  nninfwlpoimlemginf  7237  nninfwlpoim  7239  seq3id3  10598  seq3id2  10600  seq3z  10602  wrdmap  10948  fsum3cvg  11524  summodclem2a  11527  fproddccvg  11718  nninfctlemfo  12180  algfx  12193  ennnfonelemim  12584  gsumfzz  13070  ghmf1  13346  ivthreinc  14824  ivthdich  14832  reeff1oleme  14948  sin0pilem2  14958  lgsquadlem1  15234  bj-charfunbi  15373  nninfomnilem  15578  trilpolemlt1  15601  redcwlpolemeq1  15614  nconstwlpolem0  15623  nconstwlpolem  15625  neapmkvlem  15627