Theorem fveqeq2 5699

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402  ‘cfv 5372

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380

This theorem is referenced by:  uchoice  6361  suppfnss  6487  suppssfvg  6493  2omap  7308  nninfninc  7453  nnnninfeq2  7459  fodjum  7476  fodju0  7477  fodjuomnilemres  7478  fodjumkvlemres  7489  fodjumkv  7490  enmkvlem  7491  enwomnilem  7499  nninfwlporlemd  7502  nninfwlpoimlemginf  7506  nninfwlpoim  7509  nninfinfwlpo  7510  seq3id3  10939  seq3id2  10941  seq3z  10943  hashfibclem  11260  hashfibc  11261  wrdmap  11314  wrdl1s1  11376  wrdind  11472  wrd2ind  11473  reuccatpfxs1lem  11496  reuccatpfxs1  11497  fsum3cvg  12123  summodclem2a  12126  fproddccvg  12317  nninfctlemfo  12795  algfx  12808  ballotfilemelo  13200  ballotfilemfmpn  13212  ballotfilemiex  13222  ballotfilemi1  13223  ballotfilemii  13224  ballotfilemscl  13225  ballotfilemimin  13227  ballotfilemfrcn0  13251  ballotfilemirc  13253  ballotfi  13260  ennnfonelemim  13293  ghmf1  14053  mplsubgfilemcl  15013  ivthreinc  15669  ivthdich  15677  reeff1oleme  15796  sin0pilem2  15806  lgsquadlem1  16110  gropd  16202  grstructd2dom  16203  uhgr2edg  16361  usgredg2v  16379  ushgredgedgloop  16383  vtxlpfi  16445  vtxdumgrfival  16453  isclwwlkng  16561  clwwlkn1loopb  16575  s2elclwwlknon2  16591  bj-charfunbi  16751  pw1map  16939  nninfomnilem  16966  nnnninfex  16970  trilpolemlt1  16995  redcwlpolemeq1  17009  nconstwlpolem0  17018  nconstwlpolem  17020  neapmkvlem  17022