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  28363  uhgrun  28365  uhgrstrrepe  28369  isumgrs  28387  upgrun  28409  umgrun  28411  wksfval  28897  wlkres  28958  ajfval  30093  chscllem4  30924  lindfpropd  32529  ply1degltdimlem  32738  fedgmullem1  32745  rrhf  33009  sibff  33366  sibfof  33370  orvcval4  33490  bj-finsumval0  36214  matunitlindflem2  36533  poimirlem9  36545  isbnd3  36700  prdsbnd  36709  heibor  36737  elghomlem1OLD  36801  evlsvvval  41183  cnfsmf  45504  upwlksfval  46561  resmgmhm2b  46618  rngqiprngghm  46832  zrtermorngc  46947  zrtermoringc  47016