Theorem fveqeq2 5642

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1395   ` cfv 5322

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3890  df-br 4085  df-iota 5282  df-fv 5330

This theorem is referenced by:  uchoice  6293  nninfninc  7311  nnnninfeq2  7317  fodjum  7334  fodju0  7335  fodjuomnilemres  7336  fodjumkvlemres  7347  fodjumkv  7348  enmkvlem  7349  enwomnilem  7357  nninfwlporlemd  7360  nninfwlpoimlemginf  7364  nninfwlpoim  7367  nninfinfwlpo  7368  seq3id3  10774  seq3id2  10776  seq3z  10778  wrdmap  11132  wrdl1s1  11194  wrdind  11290  wrd2ind  11291  reuccatpfxs1lem  11314  reuccatpfxs1  11315  fsum3cvg  11926  summodclem2a  11929  fproddccvg  12120  nninfctlemfo  12598  algfx  12611  ennnfonelemim  13032  gsumfzz  13565  ghmf1  13847  mplsubgfilemcl  14700  ivthreinc  15356  ivthdich  15364  reeff1oleme  15483  sin0pilem2  15493  lgsquadlem1  15793  gropd  15885  grstructd2dom  15886  uhgr2edg  16041  usgredg2v  16059  ushgredgedgloop  16063  vtxlpfi  16092  vtxdumgrfival  16100  isclwwlkng  16191  clwwlkn1loopb  16205  s2elclwwlknon2  16221  bj-charfunbi  16316  2omap  16504  pw1map  16506  nninfomnilem  16530  nnnninfex  16534  trilpolemlt1  16555  redcwlpolemeq1  16568  nconstwlpolem0  16577  nconstwlpolem  16579  neapmkvlem  16581