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 207   = wceq 1547  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907  df-f 6496

This theorem is referenced by:  feq3dd  6649  feq123d  6651  fsn2  7085  fsng  7086  fsnunf  7136  funcres2b  17862  funcres2  17863  funcres2c  17868  catciso  18076  hofcl  18223  yonedalem4c  18241  yonedalem3b  18243  yonedainv  18245  gsumress  18648  resmgmhm2b  18679  resmhm2b  18788  pwsdiagmhm  18797  frmdup3lem  18832  frmdup3  18833  isghmOLD  19189  frgpup3lem  19750  gsumzsubmcl  19891  dmdprd  19973  zrtermorngc  20622  zrtermoringc  20654  imadrhmcl  20776  rngqiprngghm  21299  frlmup2  21781  evlsvvval  22076  scmatghm  22523  scmatmhm  22524  mdetdiaglem  22588  cnpf2  23240  2ndcctbss  23445  1stcelcls  23451  uptx  23615  txcn  23616  tsmssubm  24133  cnextucn  24292  pi1addf  25039  caufval  25267  equivcau  25292  lmcau  25305  plypf1  26202  coef2  26221  ulmval  26370  uhgr0vb  29166  uhgrun  29168  uhgrstrrepe  29172  isumgrs  29190  upgrun  29212  umgrun  29214  wksfval  29703  wlkres  29762  ajfval  30905  chscllem4  31736  rlocf1  33361  imasmhm  33444  imasghm  33445  imasrhm  33446  lindfpropd  33472  ply1degltdimlem  33813  fedgmullem1  33820  rrhf  34189  sibff  34527  sibfof  34531  orvcval4  34652  bj-finsumval0  37652  matunitlindflem2  37991  poimirlem9  38003  isbnd3  38158  prdsbnd  38167  heibor  38195  elghomlem1OLD  38259  aks6d1c6lem2  42663  aks6d1c6lem3  42664  aks6d1c6isolem2  42667  aks6d1c6lem5  42669  cnfsmf  47190  upwlksfval  48633