Theorem feq2d 5333

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348  ⟶wf 5192

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-fn 5199  df-f 5200

This theorem is referenced by:  feq12d  5335  ffdm  5366  fsng  5667  issmo2  6266  qliftf  6596  elpm2r  6642  casef  7063  fseq1p1m1  10043  fseq1m1p1  10044  seqf  10410  seqf2  10413  intopsn  12614  lmtopcnp  13009  ellimc3apf  13388  dvidlemap  13419  dviaddf  13428  dvimulf  13429  dvcjbr  13431  dvcj  13432  dvrecap  13436  dvmptclx  13439