Theorem feq2d 5437

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1375  ⟶wf 5290

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 1473  ax-gen 1475  ax-4 1536  ax-17 1552  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-cleq 2202  df-fn 5297  df-f 5298

This theorem is referenced by:  feq12d  5439  ffdm  5470  fsng  5781  issmo2  6405  qliftf  6737  elpm2r  6783  casef  7223  fseq1p1m1  10258  fseq1m1p1  10259  seqf  10653  seqf2  10657  seqf1og  10710  iswrdinn0  11043  wrdf  11044  iswrdiz  11045  wrdffz  11059  wrdnval  11068  swrdf  11153  swrdwrdsymbg  11162  cats1un  11219  s2dmg  11288  intopsn  13366  gsumprval  13398  resmhm  13486  gsumwsubmcl  13495  gsumwmhm  13497  isghm  13746  resghm  13763  psrelbasfi  14605  lmtopcnp  14889  ellimc3apf  15299  dvidlemap  15330  dvidrelem  15331  dvidsslem  15332  dviaddf  15344  dvimulf  15345  dvcjbr  15347  dvcj  15348  dvrecap  15352  dvmptclx  15357  uhgrm  15843  wrdupgren  15861  upgrfnen  15863  wrdumgren  15871  umgrfnen  15873