Theorem fveqeq2 5587

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373  ‘cfv 5272

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280

This theorem is referenced by:  uchoice  6225  nninfninc  7227  nnnninfeq2  7233  fodjum  7250  fodju0  7251  fodjuomnilemres  7252  fodjumkvlemres  7263  fodjumkv  7264  enmkvlem  7265  enwomnilem  7273  nninfwlporlemd  7276  nninfwlpoimlemginf  7280  nninfwlpoim  7283  nninfinfwlpo  7284  seq3id3  10671  seq3id2  10673  seq3z  10675  wrdmap  11027  wrdl1s1  11087  fsum3cvg  11722  summodclem2a  11725  fproddccvg  11916  nninfctlemfo  12394  algfx  12407  ennnfonelemim  12828  gsumfzz  13360  ghmf1  13642  mplsubgfilemcl  14494  ivthreinc  15150  ivthdich  15158  reeff1oleme  15277  sin0pilem2  15287  lgsquadlem1  15587  gropd  15677  grstructd2dom  15678  bj-charfunbi  15784  2omap  15969  nninfomnilem  15992  nnnninfex  15996  trilpolemlt1  16017  redcwlpolemeq1  16030  nconstwlpolem0  16039  nconstwlpolem  16041  neapmkvlem  16043