Theorem feq3d 6647

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918  df-f 6496

This theorem is referenced by:  feq3dd  6649  feq123d  6651  fsn2  7081  fsng  7082  fsnunf  7131  funcres2b  17821  funcres2  17822  funcres2c  17827  catciso  18035  hofcl  18182  yonedalem4c  18200  yonedalem3b  18202  yonedainv  18204  gsumress  18607  resmgmhm2b  18638  resmhm2b  18747  pwsdiagmhm  18756  frmdup3lem  18791  frmdup3  18792  isghmOLD  19145  frgpup3lem  19706  gsumzsubmcl  19847  dmdprd  19929  zrtermorngc  20576  zrtermoringc  20608  imadrhmcl  20730  rngqiprngghm  21254  frlmup2  21754  evlsvvval  22048  scmatghm  22477  scmatmhm  22478  mdetdiaglem  22542  cnpf2  23194  2ndcctbss  23399  1stcelcls  23405  uptx  23569  txcn  23570  tsmssubm  24087  cnextucn  24246  pi1addf  25003  caufval  25231  equivcau  25256  lmcau  25269  plypf1  26173  coef2  26192  ulmval  26345  uhgr0vb  29145  uhgrun  29147  uhgrstrrepe  29151  isumgrs  29169  upgrun  29191  umgrun  29193  wksfval  29683  wlkres  29742  ajfval  30884  chscllem4  31715  rlocf1  33355  imasmhm  33435  imasghm  33436  imasrhm  33437  lindfpropd  33463  ply1degltdimlem  33779  fedgmullem1  33786  rrhf  34155  sibff  34493  sibfof  34497  orvcval4  34618  bj-finsumval0  37486  matunitlindflem2  37814  poimirlem9  37826  isbnd3  37981  prdsbnd  37990  heibor  38018  elghomlem1OLD  38082  aks6d1c6lem2  42421  aks6d1c6lem3  42422  aks6d1c6isolem2  42425  aks6d1c6lem5  42427  cnfsmf  46980  upwlksfval  48377