Theorem feq3d 6571

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-f 6422

This theorem is referenced by:  feq123d  6573  fsn2  6990  fsng  6991  fsnunf  7039  funcres2b  17528  funcres2  17529  funcres2c  17533  catciso  17742  hofcl  17893  yonedalem4c  17911  yonedalem3b  17913  yonedainv  17915  gsumress  18281  resmhm2b  18376  pwsdiagmhm  18384  frmdup3lem  18420  frmdup3  18421  isghm  18749  frgpup3lem  19298  gsumzsubmcl  19434  dmdprd  19516  frlmup2  20916  scmatghm  21590  scmatmhm  21591  mdetdiaglem  21655  cnpf2  22309  2ndcctbss  22514  1stcelcls  22520  uptx  22684  txcn  22685  tsmssubm  23202  cnextucn  23363  pi1addf  24116  caufval  24344  equivcau  24369  lmcau  24382  plypf1  25278  coef2  25297  ulmval  25444  uhgr0vb  27345  uhgrun  27347  uhgrstrrepe  27351  isumgrs  27369  upgrun  27391  umgrun  27393  wksfval  27879  wlkres  27940  ajfval  29072  chscllem4  29903  lindfpropd  31478  fedgmullem1  31612  rrhf  31848  sibff  32203  sibfof  32207  orvcval4  32327  bj-finsumval0  35383  matunitlindflem2  35701  poimirlem9  35713  isbnd3  35869  prdsbnd  35878  heibor  35906  elghomlem1OLD  35970  selvval2lem4  40154  cnfsmf  44163  upwlksfval  45185  resmgmhm2b  45242  zrtermorngc  45447  zrtermoringc  45516