Theorem feq3d 6641

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915  df-f 6490

This theorem is referenced by:  feq3dd  6643  feq123d  6645  fsn2  7075  fsng  7076  fsnunf  7125  funcres2b  17806  funcres2  17807  funcres2c  17812  catciso  18020  hofcl  18167  yonedalem4c  18185  yonedalem3b  18187  yonedainv  18189  gsumress  18592  resmgmhm2b  18623  resmhm2b  18732  pwsdiagmhm  18741  frmdup3lem  18776  frmdup3  18777  isghmOLD  19130  frgpup3lem  19691  gsumzsubmcl  19832  dmdprd  19914  zrtermorngc  20560  zrtermoringc  20592  imadrhmcl  20714  rngqiprngghm  21238  frlmup2  21738  scmatghm  22449  scmatmhm  22450  mdetdiaglem  22514  cnpf2  23166  2ndcctbss  23371  1stcelcls  23377  uptx  23541  txcn  23542  tsmssubm  24059  cnextucn  24218  pi1addf  24975  caufval  25203  equivcau  25228  lmcau  25241  plypf1  26145  coef2  26164  ulmval  26317  uhgr0vb  29052  uhgrun  29054  uhgrstrrepe  29058  isumgrs  29076  upgrun  29098  umgrun  29100  wksfval  29590  wlkres  29649  ajfval  30791  chscllem4  31622  rlocf1  33247  imasmhm  33326  imasghm  33327  imasrhm  33328  lindfpropd  33354  ply1degltdimlem  33656  fedgmullem1  33663  rrhf  34032  sibff  34370  sibfof  34374  orvcval4  34495  bj-finsumval0  37350  matunitlindflem2  37677  poimirlem9  37689  isbnd3  37844  prdsbnd  37853  heibor  37881  elghomlem1OLD  37945  aks6d1c6lem2  42284  aks6d1c6lem3  42285  aks6d1c6isolem2  42288  aks6d1c6lem5  42290  evlsvvval  42681  cnfsmf  46862  upwlksfval  48259