Theorem feq3d 5945

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5808

This theorem is referenced by:  feq123d  5947  fsn2  6309  fsng  6310  fsnunf  6356  funcres2b  16380  funcres2  16381  funcres2c  16384  catciso  16580  hofcl  16722  yonedalem4c  16740  yonedalem3b  16742  yonedainv  16744  gsumress  17099  resmhm2b  17184  pwsdiagmhm  17192  frmdup3lem  17226  frmdup3  17227  isghm  17483  frgpup3lem  18013  gsumzsubmcl  18141  dmdprd  18220  frlmup2  19957  scmatghm  20158  scmatmhm  20159  mdetdiaglem  20223  cnpf2  20864  2ndcctbss  21068  1stcelcls  21074  uptx  21238  txcn  21239  tsmssubm  21756  cnextucn  21917  pi1addf  22655  caufval  22881  equivcau  22906  lmcau  22919  plypf1  23772  coef2  23791  ulmval  23938  uhgr0vb  25738  uhgrun  25740  uhgrstrrepe  25745  isumgrs  25762  upgrun  25784  umgrun  25786  uhgrac  25834  ajfval  27048  chscllem4  27883  rrhf  29370  sibff  29725  sibfof  29729  orvcval4  29849  bj-finsumval0  32324  matunitlindflem2  32576  poimirlem9  32588  isbnd3  32753  prdsbnd  32762  heibor  32790  elghomlem1OLD  32854  cnfsmf  39627  1wlksfval  40811  wlksfval  40812  1wlkres  40879  resmgmhm2b  41590  zrtermorngc  41793  zrtermoringc  41862