Theorem feq3d 6705

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-f 6548

This theorem is referenced by:  feq123d  6707  fsn2  7134  fsng  7135  fsnunf  7183  funcres2b  17847  funcres2  17848  funcres2c  17852  catciso  18061  hofcl  18212  yonedalem4c  18230  yonedalem3b  18232  yonedainv  18234  gsumress  18601  resmhm2b  18703  pwsdiagmhm  18712  frmdup3lem  18747  frmdup3  18748  isghm  19092  frgpup3lem  19645  gsumzsubmcl  19786  dmdprd  19868  imadrhmcl  20413  frlmup2  21354  scmatghm  22035  scmatmhm  22036  mdetdiaglem  22100  cnpf2  22754  2ndcctbss  22959  1stcelcls  22965  uptx  23129  txcn  23130  tsmssubm  23647  cnextucn  23808  pi1addf  24563  caufval  24792  equivcau  24817  lmcau  24830  plypf1  25726  coef2  25745  ulmval  25892  uhgr0vb  28332  uhgrun  28334  uhgrstrrepe  28338  isumgrs  28356  upgrun  28378  umgrun  28380  wksfval  28866  wlkres  28927  ajfval  30062  chscllem4  30893  lindfpropd  32498  ply1degltdimlem  32707  fedgmullem1  32714  rrhf  32978  sibff  33335  sibfof  33339  orvcval4  33459  bj-finsumval0  36166  matunitlindflem2  36485  poimirlem9  36497  isbnd3  36652  prdsbnd  36661  heibor  36689  elghomlem1OLD  36753  evlsvvval  41135  cnfsmf  45456  upwlksfval  46513  resmgmhm2b  46570  rngqiprngghm  46784  zrtermorngc  46899  zrtermoringc  46968