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  10188  fseq1m1p1  10189  seqf  10575  seqf2  10579  seqf1og  10632  iswrdinn0  10959  wrdf  10960  iswrdiz  10961  wrdffz  10975  wrdnval  10984  intopsn  13071  gsumprval  13103  resmhm  13191  gsumwsubmcl  13200  gsumwmhm  13202  isghm  13451  resghm  13468  psrelbasfi  14310  lmtopcnp  14594  ellimc3apf  15004  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dviaddf  15049  dvimulf  15050  dvcjbr  15052  dvcj  15053  dvrecap  15057  dvmptclx  15062