Theorem feq2d 5472

Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
feq2d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
feq2d	⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))

Proof of Theorem feq2d

Step	Hyp	Ref	Expression
1		feq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		feq2 5468	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  ⟶wf 5324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-cleq 2223  df-fn 5331  df-f 5332

This theorem is referenced by:  feq12d  5474  ffdm  5507  fsng  5823  fsn2g  5825  issmo2  6460  qliftf  6794  elpm2r  6840  casef  7292  fseq1p1m1  10334  fseq1m1p1  10335  seqf  10732  seqf2  10736  seqf1og  10789  iswrdinn0  11127  wrdf  11128  iswrdiz  11129  wrdffz  11143  ffz0iswrdnn0  11149  wrdnval  11153  ccatalpha  11199  swrdf  11245  swrdwrdsymbg  11254  cats1un  11311  s2dmg  11380  intopsn  13473  gsumprval  13505  resmhm  13593  gsumwsubmcl  13602  gsumwmhm  13604  isghm  13853  resghm  13870  gsumsplit0  13956  psrelbasfi  14719  lmtopcnp  15003  ellimc3apf  15413  dvidlemap  15444  dvidrelem  15445  dvidsslem  15446  dviaddf  15458  dvimulf  15459  dvcjbr  15461  dvcj  15462  dvrecap  15466  dvmptclx  15471  uhgrm  15958  wrdupgren  15976  upgrfnen  15978  wrdumgren  15986  umgrfnen  15988  upgr2wlkdc  16257  wlkres  16259  gfsumval  16748  gsumgfsum  16752