Theorem feq2d 5467

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

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

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 5327  df-f 5328

This theorem is referenced by:  feq12d  5469  ffdm  5502  fsng  5816  issmo2  6450  qliftf  6784  elpm2r  6830  casef  7281  fseq1p1m1  10322  fseq1m1p1  10323  seqf  10719  seqf2  10723  seqf1og  10776  iswrdinn0  11111  wrdf  11112  iswrdiz  11113  wrdffz  11127  ffz0iswrdnn0  11133  wrdnval  11137  ccatalpha  11183  swrdf  11229  swrdwrdsymbg  11238  cats1un  11295  s2dmg  11364  intopsn  13443  gsumprval  13475  resmhm  13563  gsumwsubmcl  13572  gsumwmhm  13574  isghm  13823  resghm  13840  psrelbasfi  14683  lmtopcnp  14967  ellimc3apf  15377  dvidlemap  15408  dvidrelem  15409  dvidsslem  15410  dviaddf  15422  dvimulf  15423  dvcjbr  15425  dvcj  15426  dvrecap  15430  dvmptclx  15435  uhgrm  15922  wrdupgren  15940  upgrfnen  15942  wrdumgren  15950  umgrfnen  15952  upgr2wlkdc  16186  wlkres  16188  gfsumval  16630  gsumgfsum  16634