Theorem feq3d 6636

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

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

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 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919  df-f 6485

This theorem is referenced by:  feq3dd  6638  feq123d  6640  fsn2  7069  fsng  7070  fsnunf  7119  funcres2b  17801  funcres2  17802  funcres2c  17807  catciso  18015  hofcl  18162  yonedalem4c  18180  yonedalem3b  18182  yonedainv  18184  gsumress  18587  resmgmhm2b  18618  resmhm2b  18727  pwsdiagmhm  18736  frmdup3lem  18771  frmdup3  18772  isghmOLD  19126  frgpup3lem  19687  gsumzsubmcl  19828  dmdprd  19910  zrtermorngc  20556  zrtermoringc  20588  imadrhmcl  20710  rngqiprngghm  21234  frlmup2  21734  scmatghm  22446  scmatmhm  22447  mdetdiaglem  22511  cnpf2  23163  2ndcctbss  23368  1stcelcls  23374  uptx  23538  txcn  23539  tsmssubm  24056  cnextucn  24215  pi1addf  24972  caufval  25200  equivcau  25225  lmcau  25238  plypf1  26142  coef2  26161  ulmval  26314  uhgr0vb  29048  uhgrun  29050  uhgrstrrepe  29054  isumgrs  29072  upgrun  29094  umgrun  29096  wksfval  29586  wlkres  29645  ajfval  30784  chscllem4  31615  rlocf1  33235  imasmhm  33314  imasghm  33315  imasrhm  33316  lindfpropd  33342  ply1degltdimlem  33630  fedgmullem1  33637  rrhf  34006  sibff  34344  sibfof  34348  orvcval4  34469  bj-finsumval0  37318  matunitlindflem2  37656  poimirlem9  37668  isbnd3  37823  prdsbnd  37832  heibor  37860  elghomlem1OLD  37924  aks6d1c6lem2  42203  aks6d1c6lem3  42204  aks6d1c6isolem2  42207  aks6d1c6lem5  42209  evlsvvval  42595  cnfsmf  46777  upwlksfval  48165