Theorem feq3d 6241

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1653  ⟶wf 6095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781  df-f 6103

This theorem is referenced by:  feq123d  6243  fsn2  6628  fsng  6629  fsnunf  6678  funcres2b  16868  funcres2  16869  funcres2c  16872  catciso  17068  hofcl  17211  yonedalem4c  17229  yonedalem3b  17231  yonedainv  17233  gsumress  17588  resmhm2b  17673  pwsdiagmhm  17681  frmdup3lem  17716  frmdup3  17717  isghm  17970  frgpup3lem  18502  gsumzsubmcl  18630  dmdprd  18710  frlmup2  20460  scmatghm  20662  scmatmhm  20663  mdetdiaglem  20727  cnpf2  21380  2ndcctbss  21584  1stcelcls  21590  uptx  21754  txcn  21755  tsmssubm  22271  cnextucn  22432  pi1addf  23171  caufval  23398  equivcau  23423  lmcau  23436  plypf1  24306  coef2  24325  ulmval  24472  uhgr0vb  26299  uhgrun  26301  uhgrstrrepe  26305  isumgrs  26323  upgrun  26345  umgrun  26347  wksfval  26851  wlkres  26913  wlkresOLD  26915  ajfval  28181  chscllem4  29016  rrhf  30550  sibff  30906  sibfof  30910  orvcval4  31031  bj-finsumval0  33638  matunitlindflem2  33887  poimirlem9  33899  isbnd3  34062  prdsbnd  34071  heibor  34099  elghomlem1OLD  34163  cnfsmf  41683  upwlksfval  42503  resmgmhm2b  42587  zrtermorngc  42788  zrtermoringc  42857