Theorem feq2d 5325

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1343  ⟶wf 5184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-fn 5191  df-f 5192

This theorem is referenced by:  feq12d  5327  ffdm  5358  fsng  5658  issmo2  6257  qliftf  6586  elpm2r  6632  casef  7053  fseq1p1m1  10029  fseq1m1p1  10030  seqf  10396  seqf2  10399  intopsn  12598  lmtopcnp  12900  ellimc3apf  13279  dvidlemap  13310  dviaddf  13319  dvimulf  13320  dvcjbr  13322  dvcj  13323  dvrecap  13327  dvmptclx  13330