Theorem feq2d 5368

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

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

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 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-fn 5234  df-f 5235

This theorem is referenced by:  feq12d  5370  ffdm  5401  fsng  5705  issmo2  6308  qliftf  6638  elpm2r  6684  casef  7105  fseq1p1m1  10112  fseq1m1p1  10113  seqf  10479  seqf2  10482  intopsn  12809  resmhm  12905  isghm  13143  resghm  13160  lmtopcnp  14147  ellimc3apf  14526  dvidlemap  14557  dviaddf  14566  dvimulf  14567  dvcjbr  14569  dvcj  14570  dvrecap  14574  dvmptclx  14577