Theorem feq3d 6694

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896  df-f 6542

This theorem is used by:  feq3dd  6696  feq123d  6698  fsn2  7137  fsng  7138  fsnunf  7190  funcres2b  18077  funcres2  18078  funcres2c  18083  catciso  18291  hofcl  18438  yonedalem4c  18456  yonedalem3b  18458  yonedainv  18460  gsumress  18876  resmgmhm2b  18907  resmhm2b  19023  pwsdiagmhm  19032  frmdup3lem  19067  frmdup3  19068  frgpup3lem  19996  gsumzsubmcl  20137  dmdprd  20219  zrtermorngc  20900  zrtermoringc  20932  imadrhmcl  21059  rngqiprngghm  21600  frlmup2  22110  evlsvvval  22407  scmatghm  22853  scmatmhm  22854  mdetdiaglem  22918  matunitlindflem2  23000  cnpf2  23573  2ndcctbss  23779  1stcelcls  23785  uptx  23949  txcn  23950  tsmssubm  24467  cnextucn  24626  pi1addf  25373  caufval  25601  equivcau  25626  lmcau  25639  plypf1  26536  coef2  26555  ulmval  26712  uhgr0vb  29655  uhgrun  29657  uhgrstrrepe  29661  isumgrs  29679  upgrun  29701  umgrun  29703  wksfval  30195  wlkres  30254  ajfval  31416  chscllem4  32247  rlocf1  33881  imasmhm  33961  imasghm  33962  imasrhm  33963  lindfpropd  33983  ply1degltdimlem  34300  fedgmullem1  34307  rrhf  34676  sibff  35014  sibfof  35018  orvcval4  35139  bj-finsumval0  38299  poimirlem9  38640  isbnd3  38811  prdsbnd  38820  heibor  38848  elghomlem1OLD  38912  aks6d1c6lem2  43314  aks6d1c6lem3  43315  aks6d1c6isolem2  43318  aks6d1c6lem5  43320  cnfsmf  47843  upwlksfval  49326  parmapfunc2  50867  parmapfunc  50868