Theorem fveqeq2 5684

Description: Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.)

Assertion

Ref	Expression
fveqeq2	|- ( A = B -> ( ( F ` A ) = C <-> ( F ` B ) = C ) )

Proof of Theorem fveqeq2

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( A = B -> A = B )
2	1	fveqeq2d 5683	1 |- ( A = B -> ( ( F ` A ) = C <-> ( F ` B ) = C ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   ` cfv 5357

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365

This theorem is referenced by:  uchoice  6344  suppfnss  6470  suppssfvg  6476  2omap  7282  nninfninc  7427  nnnninfeq2  7433  fodjum  7450  fodju0  7451  fodjuomnilemres  7452  fodjumkvlemres  7463  fodjumkv  7464  enmkvlem  7465  enwomnilem  7473  nninfwlporlemd  7476  nninfwlpoimlemginf  7480  nninfwlpoim  7483  nninfinfwlpo  7484  seq3id3  10910  seq3id2  10912  seq3z  10914  hashfibclem  11231  hashfibc  11232  wrdmap  11281  wrdl1s1  11343  wrdind  11439  wrd2ind  11440  reuccatpfxs1lem  11463  reuccatpfxs1  11464  fsum3cvg  12089  summodclem2a  12092  fproddccvg  12283  nninfctlemfo  12761  algfx  12774  ballotfilemelo  13166  ballotfilemfmpn  13178  ballotfilemiex  13188  ballotfilemi1  13189  ballotfilemii  13190  ballotfilemscl  13191  ballotfilemimin  13193  ballotfilemfrcn0  13217  ballotfilemirc  13219  ballotfi  13226  ennnfonelemim  13259  gsumfzz  13750  ghmf1  14026  mplsubgfilemcl  14980  ivthreinc  15636  ivthdich  15644  reeff1oleme  15763  sin0pilem2  15773  lgsquadlem1  16076  gropd  16168  grstructd2dom  16169  uhgr2edg  16327  usgredg2v  16345  ushgredgedgloop  16349  vtxlpfi  16411  vtxdumgrfival  16419  isclwwlkng  16527  clwwlkn1loopb  16541  s2elclwwlknon2  16557  bj-charfunbi  16707  pw1map  16895  nninfomnilem  16922  nnnninfex  16926  trilpolemlt1  16951  redcwlpolemeq1  16965  nconstwlpolem0  16975  nconstwlpolem  16977  neapmkvlem  16979