Theorem feq2d 5392

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-fn 5258  df-f 5259

This theorem is referenced by:  feq12d  5394  ffdm  5425  fsng  5732  issmo2  6344  qliftf  6676  elpm2r  6722  casef  7149  fseq1p1m1  10163  fseq1m1p1  10164  seqf  10538  seqf2  10542  seqf1og  10595  iswrdinn0  10922  wrdf  10923  iswrdiz  10924  wrdffz  10938  wrdnval  10947  intopsn  12953  gsumprval  12985  resmhm  13062  gsumwsubmcl  13071  gsumwmhm  13073  isghm  13316  resghm  13333  lmtopcnp  14429  ellimc3apf  14839  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dviaddf  14884  dvimulf  14885  dvcjbr  14887  dvcj  14888  dvrecap  14892  dvmptclx  14897