Theorem feq2d 5470

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-fn 5329  df-f 5330

This theorem is referenced by:  feq12d  5472  ffdm  5505  fsng  5820  fsn2g  5822  issmo2  6455  qliftf  6789  elpm2r  6835  casef  7287  fseq1p1m1  10329  fseq1m1p1  10330  seqf  10727  seqf2  10731  seqf1og  10784  iswrdinn0  11119  wrdf  11120  iswrdiz  11121  wrdffz  11135  ffz0iswrdnn0  11141  wrdnval  11145  ccatalpha  11191  swrdf  11237  swrdwrdsymbg  11246  cats1un  11303  s2dmg  11372  intopsn  13452  gsumprval  13484  resmhm  13572  gsumwsubmcl  13581  gsumwmhm  13583  isghm  13832  resghm  13849  gsumsplit0  13935  psrelbasfi  14693  lmtopcnp  14977  ellimc3apf  15387  dvidlemap  15418  dvidrelem  15419  dvidsslem  15420  dviaddf  15432  dvimulf  15433  dvcjbr  15435  dvcj  15436  dvrecap  15440  dvmptclx  15445  uhgrm  15932  wrdupgren  15950  upgrfnen  15952  wrdumgren  15960  umgrfnen  15962  upgr2wlkdc  16231  wlkres  16233  gfsumval  16701  gsumgfsum  16705