Theorem feq2d 5519

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402  ⟶wf 5371

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5378  df-f 5379

This theorem is referenced by:  feq12d  5521  ffdm  5556  fsng  5875  fsn2g  5877  issmo2  6554  qliftf  6888  elpm2r  6934  casef  7422  fseq1p1m1  10484  fseq1m1p1  10485  seqf  10884  seqf2  10888  seqf1og  10941  iswrdinn0  11292  wrdf  11293  iswrdiz  11294  wrdffz  11308  ffz0iswrdnn0  11314  wrdnval  11318  ccatalpha  11364  swrdf  11410  swrdwrdsymbg  11419  cats1un  11476  s2dmg  11545  intopsn  13670  resmhm  13777  gzsumwsubmcl  13784  gzsumwmhm  13786  isghm  14029  resghm  14046  gzsumsplit0  14131  gsumvalfi  14135  gzsumgsum  14138  psrelbasfi  15050  lmtopcnp  15334  ellimc3apf  15744  dvidlemap  15775  dvidrelem  15776  dvidsslem  15777  dviaddf  15789  dvimulf  15790  dvcjbr  15792  dvcj  15793  dvrecap  15797  dvmptclx  15802  uhgrm  16302  wrdupgren  16320  upgrfnen  16322  wrdumgren  16330  umgrfnen  16332  upgr2wlkdc  16601  wlkres  16603