Theorem feq2d 5216

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1312  ⟶wf 5075

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-17 1487  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-cleq 2106  df-fn 5082  df-f 5083

This theorem is referenced by:  feq12d  5218  ffdm  5249  fsng  5545  issmo2  6138  qliftf  6466  elpm2r  6512  casef  6923  fseq1p1m1  9761  fseq1m1p1  9762  seqf  10121  seqf2  10124  lmtopcnp  12255  ellimc3apf  12579  dvidlemap  12609  dviaddf  12616