Theorem feq3d 6723

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979  df-f 6566

This theorem is referenced by:  feq123d  6725  fsn2  7155  fsng  7156  fsnunf  7204  funcres2b  17947  funcres2  17948  funcres2c  17954  catciso  18164  hofcl  18315  yonedalem4c  18333  yonedalem3b  18335  yonedainv  18337  gsumress  18707  resmgmhm2b  18738  resmhm2b  18847  pwsdiagmhm  18856  frmdup3lem  18891  frmdup3  18892  isghmOLD  19246  frgpup3lem  19809  gsumzsubmcl  19950  dmdprd  20032  zrtermorngc  20659  zrtermoringc  20691  imadrhmcl  20814  rngqiprngghm  21326  frlmup2  21836  scmatghm  22554  scmatmhm  22555  mdetdiaglem  22619  cnpf2  23273  2ndcctbss  23478  1stcelcls  23484  uptx  23648  txcn  23649  tsmssubm  24166  cnextucn  24327  pi1addf  25093  caufval  25322  equivcau  25347  lmcau  25360  plypf1  26265  coef2  26284  ulmval  26437  uhgr0vb  29103  uhgrun  29105  uhgrstrrepe  29109  isumgrs  29127  upgrun  29149  umgrun  29151  wksfval  29641  wlkres  29702  ajfval  30837  chscllem4  31668  feq3dd  32640  rlocf1  33259  imasmhm  33361  imasghm  33362  imasrhm  33363  lindfpropd  33389  ply1degltdimlem  33649  fedgmullem1  33656  rrhf  33960  sibff  34317  sibfof  34321  orvcval4  34441  bj-finsumval0  37267  matunitlindflem2  37603  poimirlem9  37615  isbnd3  37770  prdsbnd  37779  heibor  37807  elghomlem1OLD  37871  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks6d1c6isolem2  42156  aks6d1c6lem5  42158  evlsvvval  42549  cnfsmf  46695  upwlksfval  47978