Theorem feq3d 6697

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

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

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 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925  df-f 6547

This theorem is used by:  feq3dd  6699  feq123d  6701  fsn2  7139  fsng  7140  fsnunf  7190  funcres2b  17979  funcres2  17980  funcres2c  17985  catciso  18193  hofcl  18340  yonedalem4c  18358  yonedalem3b  18360  yonedainv  18362  gsumress  18769  resmgmhm2b  18800  resmhm2b  18912  pwsdiagmhm  18921  frmdup3lem  18956  frmdup3  18957  frgpup3lem  19878  gsumzsubmcl  20019  dmdprd  20101  zrtermorngc  20779  zrtermoringc  20811  imadrhmcl  20937  rngqiprngghm  21476  frlmup2  21986  evlsvvval  22281  scmatghm  22727  scmatmhm  22728  mdetdiaglem  22792  cnpf2  23444  2ndcctbss  23649  1stcelcls  23655  uptx  23819  txcn  23820  tsmssubm  24337  cnextucn  24496  pi1addf  25243  caufval  25471  equivcau  25496  lmcau  25509  plypf1  26406  coef2  26425  ulmval  26580  uhgr0vb  29459  uhgrun  29461  uhgrstrrepe  29465  isumgrs  29483  upgrun  29505  umgrun  29507  wksfval  29996  wlkres  30055  ajfval  31198  chscllem4  32029  rlocf1  33625  imasmhm  33705  imasghm  33706  imasrhm  33707  lindfpropd  33726  ply1degltdimlem  34043  fedgmullem1  34050  rrhf  34419  sibff  34758  sibfof  34762  orvcval4  34883  bj-finsumval0  37970  matunitlindflem2  38309  poimirlem9  38321  isbnd3  38476  prdsbnd  38485  heibor  38513  elghomlem1OLD  38577  aks6d1c6lem2  42979  aks6d1c6lem3  42980  aks6d1c6isolem2  42983  aks6d1c6lem5  42985  cnfsmf  47495  upwlksfval  48941