Theorem feq2d 5498

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

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

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 5357  df-f 5358

This theorem is referenced by:  feq12d  5500  ffdm  5535  fsng  5852  fsn2g  5854  issmo2  6522  qliftf  6856  elpm2r  6902  casef  7381  fseq1p1m1  10435  fseq1m1p1  10436  seqf  10833  seqf2  10837  seqf1og  10890  iswrdinn0  11237  wrdf  11238  iswrdiz  11239  wrdffz  11253  ffz0iswrdnn0  11259  wrdnval  11263  ccatalpha  11309  swrdf  11355  swrdwrdsymbg  11364  cats1un  11421  s2dmg  11490  intopsn  13601  gsumprval  13633  resmhm  13721  gsumwsubmcl  13730  gsumwmhm  13732  isghm  13981  resghm  13998  gsumsplit0  14084  psrelbasfi  14880  lmtopcnp  15164  ellimc3apf  15574  dvidlemap  15605  dvidrelem  15606  dvidsslem  15607  dviaddf  15619  dvimulf  15620  dvcjbr  15622  dvcj  15623  dvrecap  15627  dvmptclx  15632  uhgrm  16122  wrdupgren  16140  upgrfnen  16142  wrdumgren  16150  umgrfnen  16152  upgr2wlkdc  16421  wlkres  16423  gfsumval  16911  gsumgfsum  16915