Theorem feq3d 6655

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920  df-f 6504

This theorem is referenced by:  feq3dd  6657  feq123d  6659  fsn2  7091  fsng  7092  fsnunf  7141  funcres2b  17833  funcres2  17834  funcres2c  17839  catciso  18047  hofcl  18194  yonedalem4c  18212  yonedalem3b  18214  yonedainv  18216  gsumress  18619  resmgmhm2b  18650  resmhm2b  18759  pwsdiagmhm  18768  frmdup3lem  18803  frmdup3  18804  isghmOLD  19157  frgpup3lem  19718  gsumzsubmcl  19859  dmdprd  19941  zrtermorngc  20588  zrtermoringc  20620  imadrhmcl  20742  rngqiprngghm  21266  frlmup2  21766  evlsvvval  22060  scmatghm  22489  scmatmhm  22490  mdetdiaglem  22554  cnpf2  23206  2ndcctbss  23411  1stcelcls  23417  uptx  23581  txcn  23582  tsmssubm  24099  cnextucn  24258  pi1addf  25015  caufval  25243  equivcau  25268  lmcau  25281  plypf1  26185  coef2  26204  ulmval  26357  uhgr0vb  29157  uhgrun  29159  uhgrstrrepe  29163  isumgrs  29181  upgrun  29203  umgrun  29205  wksfval  29695  wlkres  29754  ajfval  30896  chscllem4  31727  rlocf1  33366  imasmhm  33446  imasghm  33447  imasrhm  33448  lindfpropd  33474  ply1degltdimlem  33799  fedgmullem1  33806  rrhf  34175  sibff  34513  sibfof  34517  orvcval4  34638  bj-finsumval0  37534  matunitlindflem2  37862  poimirlem9  37874  isbnd3  38029  prdsbnd  38038  heibor  38066  elghomlem1OLD  38130  aks6d1c6lem2  42535  aks6d1c6lem3  42536  aks6d1c6isolem2  42539  aks6d1c6lem5  42541  cnfsmf  47092  upwlksfval  48489