Theorem feq2d 5398

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364  ⟶wf 5255

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-fn 5262  df-f 5263

This theorem is referenced by:  feq12d  5400  ffdm  5431  fsng  5738  issmo2  6356  qliftf  6688  elpm2r  6734  casef  7163  fseq1p1m1  10186  fseq1m1p1  10187  seqf  10573  seqf2  10577  seqf1og  10630  iswrdinn0  10957  wrdf  10958  iswrdiz  10959  wrdffz  10973  wrdnval  10982  intopsn  13069  gsumprval  13101  resmhm  13189  gsumwsubmcl  13198  gsumwmhm  13200  isghm  13449  resghm  13466  lmtopcnp  14570  ellimc3apf  14980  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dviaddf  15025  dvimulf  15026  dvcjbr  15028  dvcj  15029  dvrecap  15033  dvmptclx  15038