Theorem feq2d 5501

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398  ⟶wf 5353

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-fn 5360  df-f 5361

This theorem is referenced by:  feq12d  5503  ffdm  5538  fsng  5855  fsn2g  5857  issmo2  6533  qliftf  6867  elpm2r  6913  casef  7392  fseq1p1m1  10453  fseq1m1p1  10454  seqf  10853  seqf2  10857  seqf1og  10910  iswrdinn0  11257  wrdf  11258  iswrdiz  11259  wrdffz  11273  ffz0iswrdnn0  11279  wrdnval  11283  ccatalpha  11329  swrdf  11375  swrdwrdsymbg  11384  cats1un  11441  s2dmg  11510  intopsn  13633  gsumprval  13665  resmhm  13745  gsumwsubmcl  13754  gsumwmhm  13756  isghm  13999  resghm  14016  gsumsplit0  14102  gfsumval  14105  gsumgfsum  14109  psrelbasfi  14960  lmtopcnp  15244  ellimc3apf  15654  dvidlemap  15685  dvidrelem  15686  dvidsslem  15687  dviaddf  15699  dvimulf  15700  dvcjbr  15702  dvcj  15703  dvrecap  15707  dvmptclx  15712  uhgrm  16202  wrdupgren  16220  upgrfnen  16222  wrdumgren  16230  umgrfnen  16232  upgr2wlkdc  16501  wlkres  16503