Theorem feq3d 6474

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 6470	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝑋⟶𝐴 ↔ 𝐹:𝑋⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ⟶wf 6320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-f 6328

This theorem is referenced by:  feq123d  6476  fsn2  6875  fsng  6876  fsnunf  6924  funcres2b  17159  funcres2  17160  funcres2c  17163  catciso  17359  hofcl  17501  yonedalem4c  17519  yonedalem3b  17521  yonedainv  17523  gsumress  17884  resmhm2b  17979  pwsdiagmhm  17987  frmdup3lem  18023  frmdup3  18024  isghm  18350  frgpup3lem  18895  gsumzsubmcl  19031  dmdprd  19113  frlmup2  20488  scmatghm  21138  scmatmhm  21139  mdetdiaglem  21203  cnpf2  21855  2ndcctbss  22060  1stcelcls  22066  uptx  22230  txcn  22231  tsmssubm  22748  cnextucn  22909  pi1addf  23652  caufval  23879  equivcau  23904  lmcau  23917  plypf1  24809  coef2  24828  ulmval  24975  uhgr0vb  26865  uhgrun  26867  uhgrstrrepe  26871  isumgrs  26889  upgrun  26911  umgrun  26913  wksfval  27399  wlkres  27460  ajfval  28592  chscllem4  29423  lindfpropd  30996  fedgmullem1  31113  rrhf  31349  sibff  31704  sibfof  31708  orvcval4  31828  bj-finsumval0  34700  matunitlindflem2  35054  poimirlem9  35066  isbnd3  35222  prdsbnd  35231  heibor  35259  elghomlem1OLD  35323  selvval2lem4  39431  cnfsmf  43374  upwlksfval  44363  resmgmhm2b  44420  zrtermorngc  44625  zrtermoringc  44694