Theorem feq2d 5419

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373  ⟶wf 5272

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-fn 5279  df-f 5280

This theorem is referenced by:  feq12d  5421  ffdm  5452  fsng  5760  issmo2  6382  qliftf  6714  elpm2r  6760  casef  7197  fseq1p1m1  10223  fseq1m1p1  10224  seqf  10616  seqf2  10620  seqf1og  10673  iswrdinn0  11006  wrdf  11007  iswrdiz  11008  wrdffz  11022  wrdnval  11031  swrdf  11116  swrdwrdsymbg  11125  intopsn  13243  gsumprval  13275  resmhm  13363  gsumwsubmcl  13372  gsumwmhm  13374  isghm  13623  resghm  13640  psrelbasfi  14482  lmtopcnp  14766  ellimc3apf  15176  dvidlemap  15207  dvidrelem  15208  dvidsslem  15209  dviaddf  15221  dvimulf  15222  dvcjbr  15224  dvcj  15225  dvrecap  15229  dvmptclx  15234  uhgrm  15718