Theorem feq2d 5495

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-fn 5354  df-f 5355

This theorem is referenced by:  feq12d  5497  ffdm  5532  fsng  5849  fsn2g  5851  issmo2  6519  qliftf  6853  elpm2r  6899  casef  7378  fseq1p1m1  10424  fseq1m1p1  10425  seqf  10822  seqf2  10826  seqf1og  10879  iswrdinn0  11222  wrdf  11223  iswrdiz  11224  wrdffz  11238  ffz0iswrdnn0  11244  wrdnval  11248  ccatalpha  11294  swrdf  11340  swrdwrdsymbg  11349  cats1un  11406  s2dmg  11475  intopsn  13569  gsumprval  13601  resmhm  13689  gsumwsubmcl  13698  gsumwmhm  13700  isghm  13949  resghm  13966  gsumsplit0  14052  psrelbasfi  14818  lmtopcnp  15102  ellimc3apf  15512  dvidlemap  15543  dvidrelem  15544  dvidsslem  15545  dviaddf  15557  dvimulf  15558  dvcjbr  15560  dvcj  15561  dvrecap  15565  dvmptclx  15570  uhgrm  16060  wrdupgren  16078  upgrfnen  16080  wrdumgren  16088  umgrfnen  16090  upgr2wlkdc  16359  wlkres  16361  gfsumval  16848  gsumgfsum  16852