Theorem feq3d 6676

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934  df-f 6518

This theorem is referenced by:  feq3dd  6678  feq123d  6680  fsn2  7111  fsng  7112  fsnunf  7162  funcres2b  17866  funcres2  17867  funcres2c  17872  catciso  18080  hofcl  18227  yonedalem4c  18245  yonedalem3b  18247  yonedainv  18249  gsumress  18616  resmgmhm2b  18647  resmhm2b  18756  pwsdiagmhm  18765  frmdup3lem  18800  frmdup3  18801  isghmOLD  19155  frgpup3lem  19714  gsumzsubmcl  19855  dmdprd  19937  zrtermorngc  20559  zrtermoringc  20591  imadrhmcl  20713  rngqiprngghm  21216  frlmup2  21715  scmatghm  22427  scmatmhm  22428  mdetdiaglem  22492  cnpf2  23144  2ndcctbss  23349  1stcelcls  23355  uptx  23519  txcn  23520  tsmssubm  24037  cnextucn  24197  pi1addf  24954  caufval  25182  equivcau  25207  lmcau  25220  plypf1  26124  coef2  26143  ulmval  26296  uhgr0vb  29006  uhgrun  29008  uhgrstrrepe  29012  isumgrs  29030  upgrun  29052  umgrun  29054  wksfval  29544  wlkres  29605  ajfval  30745  chscllem4  31576  rlocf1  33231  imasmhm  33332  imasghm  33333  imasrhm  33334  lindfpropd  33360  ply1degltdimlem  33625  fedgmullem1  33632  rrhf  33995  sibff  34334  sibfof  34338  orvcval4  34459  bj-finsumval0  37280  matunitlindflem2  37618  poimirlem9  37630  isbnd3  37785  prdsbnd  37794  heibor  37822  elghomlem1OLD  37886  aks6d1c6lem2  42166  aks6d1c6lem3  42167  aks6d1c6isolem2  42170  aks6d1c6lem5  42172  evlsvvval  42558  cnfsmf  46745  upwlksfval  48127