Theorem feq3d 6672

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  ⟶wf 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921  df-f 6521

This theorem is referenced by:  feq3dd  6674  feq123d  6676  fsn2  7114  fsng  7115  fsnunf  7165  funcres2b  17913  funcres2  17914  funcres2c  17919  catciso  18127  hofcl  18274  yonedalem4c  18292  yonedalem3b  18294  yonedainv  18296  gsumress  18699  resmgmhm2b  18730  resmhm2b  18839  pwsdiagmhm  18848  frmdup3lem  18883  frmdup3  18884  frgpup3lem  19800  gsumzsubmcl  19941  dmdprd  20023  zrtermorngc  20672  zrtermoringc  20704  imadrhmcl  20826  rngqiprngghm  21349  frlmup2  21831  evlsvvval  22126  scmatghm  22573  scmatmhm  22574  mdetdiaglem  22638  cnpf2  23290  2ndcctbss  23495  1stcelcls  23501  uptx  23665  txcn  23666  tsmssubm  24183  cnextucn  24342  pi1addf  25089  caufval  25317  equivcau  25342  lmcau  25355  plypf1  26252  coef2  26271  ulmval  26420  uhgr0vb  29219  uhgrun  29221  uhgrstrrepe  29225  isumgrs  29243  upgrun  29265  umgrun  29267  wksfval  29756  wlkres  29815  ajfval  30958  chscllem4  31789  rlocf1  33416  imasmhm  33501  imasghm  33502  imasrhm  33503  lindfpropd  33529  ply1degltdimlem  33880  fedgmullem1  33887  rrhf  34256  sibff  34594  sibfof  34598  orvcval4  34719  bj-finsumval0  37741  matunitlindflem2  38080  poimirlem9  38092  isbnd3  38247  prdsbnd  38256  heibor  38284  elghomlem1OLD  38348  aks6d1c6lem2  42752  aks6d1c6lem3  42753  aks6d1c6isolem2  42756  aks6d1c6lem5  42758  cnfsmf  47278  upwlksfval  48721