Theorem feq3d 6070

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523  ⟶wf 5922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-f 5930

This theorem is referenced by:  feq123d  6072  fsn2  6443  fsng  6444  fsnunf  6492  funcres2b  16604  funcres2  16605  funcres2c  16608  catciso  16804  hofcl  16946  yonedalem4c  16964  yonedalem3b  16966  yonedainv  16968  gsumress  17323  resmhm2b  17408  pwsdiagmhm  17416  frmdup3lem  17450  frmdup3  17451  isghm  17707  frgpup3lem  18236  gsumzsubmcl  18364  dmdprd  18443  frlmup2  20186  scmatghm  20387  scmatmhm  20388  mdetdiaglem  20452  cnpf2  21102  2ndcctbss  21306  1stcelcls  21312  uptx  21476  txcn  21477  tsmssubm  21993  cnextucn  22154  pi1addf  22893  caufval  23119  equivcau  23144  lmcau  23157  plypf1  24013  coef2  24032  ulmval  24179  uhgr0vb  26012  uhgrun  26014  uhgrstrrepe  26018  isumgrs  26036  upgrun  26058  umgrun  26060  wksfval  26561  wlkres  26623  ajfval  27792  chscllem4  28627  rrhf  30170  sibff  30526  sibfof  30530  orvcval4  30650  bj-finsumval0  33277  matunitlindflem2  33536  poimirlem9  33548  isbnd3  33713  prdsbnd  33722  heibor  33750  elghomlem1OLD  33814  cnfsmf  41270  upwlksfval  42041  resmgmhm2b  42125  zrtermorngc  42326  zrtermoringc  42395