Theorem feq3d 6587

Description: Equality deduction for functions. (Contributed by AV, 1-Jan-2020.)

Hypothesis

Ref	Expression
feq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
feq3d	⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))

Proof of Theorem feq3d

Step	Hyp	Ref	Expression
1		feq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		feq3 6583	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ⟶wf 6429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-f 6437

This theorem is referenced by:  feq123d  6589  fsn2  7008  fsng  7009  fsnunf  7057  funcres2b  17612  funcres2  17613  funcres2c  17617  catciso  17826  hofcl  17977  yonedalem4c  17995  yonedalem3b  17997  yonedainv  17999  gsumress  18366  resmhm2b  18461  pwsdiagmhm  18469  frmdup3lem  18505  frmdup3  18506  isghm  18834  frgpup3lem  19383  gsumzsubmcl  19519  dmdprd  19601  frlmup2  21006  scmatghm  21682  scmatmhm  21683  mdetdiaglem  21747  cnpf2  22401  2ndcctbss  22606  1stcelcls  22612  uptx  22776  txcn  22777  tsmssubm  23294  cnextucn  23455  pi1addf  24210  caufval  24439  equivcau  24464  lmcau  24477  plypf1  25373  coef2  25392  ulmval  25539  uhgr0vb  27442  uhgrun  27444  uhgrstrrepe  27448  isumgrs  27466  upgrun  27488  umgrun  27490  wksfval  27976  wlkres  28038  ajfval  29171  chscllem4  30002  lindfpropd  31576  fedgmullem1  31710  rrhf  31948  sibff  32303  sibfof  32307  orvcval4  32427  bj-finsumval0  35456  matunitlindflem2  35774  poimirlem9  35786  isbnd3  35942  prdsbnd  35951  heibor  35979  elghomlem1OLD  36043  selvval2lem4  40228  cnfsmf  44276  upwlksfval  45297  resmgmhm2b  45354  zrtermorngc  45559  zrtermoringc  45628