Theorem feq2d 5524

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402  ⟶wf 5376

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5383  df-f 5384

This theorem is used by:  feq12d  5526  ffdm  5561  fsng  5884  fsn2g  5886  issmo2  6564  qliftf  6898  elpm2r  6944  casef  7435  fseq1p1m1  10519  fseq1m1p1  10520  seqf  10923  seqf2  10927  seqf1og  10980  iswrdinn0  11332  wrdf  11333  iswrdiz  11334  wrdffz  11348  ffz0iswrdnn0  11354  wrdnval  11358  ccatalpha  11404  swrdf  11450  swrdwrdsymbg  11459  cats1un  11516  s2dmg  11585  intopsn  13747  resmhm  13854  gzsumwsubmcl  13861  gzsumwmhm  13863  isghm  14106  resghm  14123  gzsumsplit0  14239  gsumvalfi  14243  gzsumgsum  14246  gsummptfidmsplit  14255  psrelbasfi  15185  lmtopcnp  15488  ellimc3apf  15898  dvidlemap  15929  dvidrelem  15930  dvidsslem  15931  dviaddf  15943  dvimulf  15944  dvcjbr  15946  dvcj  15947  dvrecap  15951  dvmptclx  15956  uhgrm  16536  wrdupgren  16554  upgrfnen  16556  wrdumgren  16564  umgrfnen  16566  upgr2wlkdc  16835  wlkres  16837