Theorem feq2d 5396

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 5392	. 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  5398  ffdm  5429  fsng  5736  issmo2  6348  qliftf  6680  elpm2r  6726  casef  7155  fseq1p1m1  10171  fseq1m1p1  10172  seqf  10558  seqf2  10562  seqf1og  10615  iswrdinn0  10942  wrdf  10943  iswrdiz  10944  wrdffz  10958  wrdnval  10967  intopsn  13020  gsumprval  13052  resmhm  13129  gsumwsubmcl  13138  gsumwmhm  13140  isghm  13383  resghm  13400  lmtopcnp  14496  ellimc3apf  14906  dvidlemap  14937  dvidrelem  14938  dvidsslem  14939  dviaddf  14951  dvimulf  14952  dvcjbr  14954  dvcj  14955  dvrecap  14959  dvmptclx  14964