Theorem fveqeq2 5704

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 5703	1 |- ( A = B -> ( ( F ` A ) = C <-> ( F ` B ) = C ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   ` cfv 5377

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385

This theorem is used by:  uchoice  6371  suppfnss  6497  suppssfvg  6503  2omap  7319  nninfninc  7464  nnnninfeq2  7470  fodjum  7487  fodju0  7488  fodjuomnilemres  7489  fodjumkvlemres  7500  fodjumkv  7501  enmkvlem  7502  enwomnilem  7510  nninfwlporlemd  7513  nninfwlpoimlemginf  7517  nninfwlpoim  7520  nninfinfwlpo  7521  seq3id3  10976  seq3id2  10978  seq3z  10980  hashfibclem  11298  hashfibc  11299  wrdmap  11352  wrdl1s1  11414  wrdind  11510  wrd2ind  11511  reuccatpfxs1lem  11534  reuccatpfxs1  11535  fsum3cvg  12164  summodclem2a  12167  fproddccvg  12358  nninfctlemfo  12836  algfx  12849  ballotfilemelo  13274  ballotfilemfmpn  13286  ballotfilemiex  13296  ballotfilemi1  13297  ballotfilemii  13298  ballotfilemscl  13299  ballotfilemimin  13301  ballotfilemfrcn0  13325  ballotfilemirc  13327  ballotfi  13334  ennnfonelemim  13367  ghmf1  14129  mplsubgfilemcl  15181  ivthreinc  15837  ivthdich  15845  reeff1oleme  15964  sin0pilem2  15975  lgsquadlem1  16362  gropd  16454  grstructd2dom  16455  uhgr2edg  16613  usgredg2v  16631  ushgredgedgloop  16635  vtxlpfi  16697  vtxdumgrfival  16705  isclwwlkng  16813  clwwlkn1loopb  16827  s2elclwwlknon2  16843  bj-charfunbi  17003  pw1map  17191  nninfomnilem  17227  nnnninfex  17231  trilpolemlt1  17257  redcwlpolemeq1  17271  nconstwlpolem0  17280  nconstwlpolem  17282  neapmkvlem  17284