Theorem feq3d 6686

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916  df-f 6535

This theorem is used by:  feq3dd  6688  feq123d  6690  fsn2  7129  fsng  7130  fsnunf  7182  funcres2b  18052  funcres2  18053  funcres2c  18058  catciso  18266  hofcl  18413  yonedalem4c  18431  yonedalem3b  18433  yonedainv  18435  gsumress  18851  resmgmhm2b  18882  resmhm2b  18998  pwsdiagmhm  19007  frmdup3lem  19042  frmdup3  19043  frgpup3lem  19971  gsumzsubmcl  20112  dmdprd  20194  zrtermorngc  20875  zrtermoringc  20907  imadrhmcl  21034  rngqiprngghm  21575  frlmup2  22085  evlsvvval  22382  scmatghm  22828  scmatmhm  22829  mdetdiaglem  22893  matunitlindflem2  22975  cnpf2  23548  2ndcctbss  23754  1stcelcls  23760  uptx  23924  txcn  23925  tsmssubm  24442  cnextucn  24601  pi1addf  25348  caufval  25576  equivcau  25601  lmcau  25614  plypf1  26511  coef2  26530  ulmval  26689  uhgr0vb  29632  uhgrun  29634  uhgrstrrepe  29638  isumgrs  29656  upgrun  29678  umgrun  29680  wksfval  30172  wlkres  30231  ajfval  31393  chscllem4  32224  rlocf1  33817  imasmhm  33897  imasghm  33898  imasrhm  33899  lindfpropd  33919  ply1degltdimlem  34236  fedgmullem1  34243  rrhf  34612  sibff  34951  sibfof  34955  orvcval4  35076  bj-finsumval0  38174  poimirlem9  38515  isbnd3  38686  prdsbnd  38695  heibor  38723  elghomlem1OLD  38787  aks6d1c6lem2  43189  aks6d1c6lem3  43190  aks6d1c6isolem2  43193  aks6d1c6lem5  43195  cnfsmf  47694  upwlksfval  49177