Theorem fveqeq2 5681

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

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

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 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362

This theorem is referenced by:  uchoice  6333  suppfnss  6459  suppssfvg  6465  2omap  7271  nninfninc  7416  nnnninfeq2  7422  fodjum  7439  fodju0  7440  fodjuomnilemres  7441  fodjumkvlemres  7452  fodjumkv  7453  enmkvlem  7454  enwomnilem  7462  nninfwlporlemd  7465  nninfwlpoimlemginf  7469  nninfwlpoim  7472  nninfinfwlpo  7473  seq3id3  10890  seq3id2  10892  seq3z  10894  hashfibclem  11210  hashfibc  11211  wrdmap  11260  wrdl1s1  11322  wrdind  11418  wrd2ind  11419  reuccatpfxs1lem  11442  reuccatpfxs1  11443  fsum3cvg  12068  summodclem2a  12071  fproddccvg  12262  nninfctlemfo  12740  algfx  12753  ballotfilemelo  13145  ballotfilemfmpn  13155  ennnfonelemim  13192  gsumfzz  13725  ghmf1  14007  mplsubgfilemcl  14871  ivthreinc  15527  ivthdich  15535  reeff1oleme  15654  sin0pilem2  15664  lgsquadlem1  15967  gropd  16059  grstructd2dom  16060  uhgr2edg  16218  usgredg2v  16236  ushgredgedgloop  16240  vtxlpfi  16302  vtxdumgrfival  16310  isclwwlkng  16418  clwwlkn1loopb  16432  s2elclwwlknon2  16448  bj-charfunbi  16598  pw1map  16786  nninfomnilem  16813  nnnninfex  16817  trilpolemlt1  16842  redcwlpolemeq1  16856  nconstwlpolem0  16866  nconstwlpolem  16868  neapmkvlem  16870