Theorem feq3d 6673

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ⟶wf 6507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931  df-f 6515

This theorem is referenced by:  feq3dd  6675  feq123d  6677  fsn2  7108  fsng  7109  fsnunf  7159  funcres2b  17859  funcres2  17860  funcres2c  17865  catciso  18073  hofcl  18220  yonedalem4c  18238  yonedalem3b  18240  yonedainv  18242  gsumress  18609  resmgmhm2b  18640  resmhm2b  18749  pwsdiagmhm  18758  frmdup3lem  18793  frmdup3  18794  isghmOLD  19148  frgpup3lem  19707  gsumzsubmcl  19848  dmdprd  19930  zrtermorngc  20552  zrtermoringc  20584  imadrhmcl  20706  rngqiprngghm  21209  frlmup2  21708  scmatghm  22420  scmatmhm  22421  mdetdiaglem  22485  cnpf2  23137  2ndcctbss  23342  1stcelcls  23348  uptx  23512  txcn  23513  tsmssubm  24030  cnextucn  24190  pi1addf  24947  caufval  25175  equivcau  25200  lmcau  25213  plypf1  26117  coef2  26136  ulmval  26289  uhgr0vb  28999  uhgrun  29001  uhgrstrrepe  29005  isumgrs  29023  upgrun  29045  umgrun  29047  wksfval  29537  wlkres  29598  ajfval  30738  chscllem4  31569  rlocf1  33224  imasmhm  33325  imasghm  33326  imasrhm  33327  lindfpropd  33353  ply1degltdimlem  33618  fedgmullem1  33625  rrhf  33988  sibff  34327  sibfof  34331  orvcval4  34452  bj-finsumval0  37273  matunitlindflem2  37611  poimirlem9  37623  isbnd3  37778  prdsbnd  37787  heibor  37815  elghomlem1OLD  37879  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks6d1c6isolem2  42163  aks6d1c6lem5  42165  evlsvvval  42551  cnfsmf  46738  upwlksfval  48123