Theorem feq2d 5461

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395  ⟶wf 5314

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-fn 5321  df-f 5322

This theorem is referenced by:  feq12d  5463  ffdm  5496  fsng  5810  issmo2  6441  qliftf  6775  elpm2r  6821  casef  7263  fseq1p1m1  10298  fseq1m1p1  10299  seqf  10694  seqf2  10698  seqf1og  10751  iswrdinn0  11084  wrdf  11085  iswrdiz  11086  wrdffz  11100  ffz0iswrdnn0  11106  wrdnval  11110  swrdf  11195  swrdwrdsymbg  11204  cats1un  11261  s2dmg  11330  intopsn  13408  gsumprval  13440  resmhm  13528  gsumwsubmcl  13537  gsumwmhm  13539  isghm  13788  resghm  13805  psrelbasfi  14648  lmtopcnp  14932  ellimc3apf  15342  dvidlemap  15373  dvidrelem  15374  dvidsslem  15375  dviaddf  15387  dvimulf  15388  dvcjbr  15390  dvcj  15391  dvrecap  15395  dvmptclx  15400  uhgrm  15886  wrdupgren  15904  upgrfnen  15906  wrdumgren  15914  umgrfnen  15916  upgr2wlkdc  16096  wlkres  16098