Theorem feq3d 6716

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6554

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-f 6562

This theorem is used by:  feq3dd  6718  feq123d  6720  fsn2  7161  fsng  7162  fsnunf  7213  funcres2b  18101  funcres2  18102  funcres2c  18107  catciso  18315  hofcl  18462  yonedalem4c  18480  yonedalem3b  18482  yonedainv  18484  gsumress  18900  resmgmhm2b  18931  resmhm2b  19047  pwsdiagmhm  19056  frmdup3lem  19091  frmdup3  19092  frgpup3lem  20021  gsumzsubmcl  20162  dmdprd  20244  zrtermorngc  20925  zrtermoringc  20957  imadrhmcl  21084  rngqiprngghm  21625  frlmup2  22135  evlsvvval  22432  scmatghm  22878  scmatmhm  22879  mdetdiaglem  22943  matunitlindflem2  23025  cnpf2  23598  2ndcctbss  23804  1stcelcls  23810  uptx  23974  txcn  23975  tsmssubm  24492  cnextucn  24651  pi1addf  25398  caufval  25626  equivcau  25651  lmcau  25664  plypf1  26561  coef2  26580  ulmval  26737  uhgr0vb  29680  uhgrun  29682  uhgrstrrepe  29686  isumgrs  29704  upgrun  29726  umgrun  29728  wksfval  30220  wlkres  30279  ajfval  31441  chscllem4  32272  rlocf1  33905  imasmhm  33985  imasghm  33986  imasrhm  33987  lindfpropd  34007  ply1degltdimlem  34324  fedgmullem1  34331  rrhf  34700  sibff  35038  sibfof  35042  orvcval4  35163  bj-finsumval0  38398  poimirlem9  38739  isbnd3  38910  prdsbnd  38919  heibor  38947  elghomlem1OLD  39011  aks6d1c6lem2  43413  aks6d1c6lem3  43414  aks6d1c6isolem2  43417  aks6d1c6lem5  43419  cnfsmf  47955  upwlksfval  49438  parmapfunc2  50979  parmapfunc  50980