Theorem feq2d 5521

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

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

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 5380  df-f 5381

This theorem is used by:  feq12d  5523  ffdm  5558  fsng  5881  fsn2g  5883  issmo2  6560  qliftf  6894  elpm2r  6940  casef  7428  fseq1p1m1  10503  fseq1m1p1  10504  seqf  10903  seqf2  10907  seqf1og  10960  iswrdinn0  11311  wrdf  11312  iswrdiz  11313  wrdffz  11327  ffz0iswrdnn0  11333  wrdnval  11337  ccatalpha  11383  swrdf  11429  swrdwrdsymbg  11438  cats1un  11495  s2dmg  11564  intopsn  13689  resmhm  13796  gzsumwsubmcl  13803  gzsumwmhm  13805  isghm  14048  resghm  14065  gzsumsplit0  14150  gsumvalfi  14154  gzsumgsum  14157  psrelbasfi  15069  lmtopcnp  15353  ellimc3apf  15763  dvidlemap  15794  dvidrelem  15795  dvidsslem  15796  dviaddf  15808  dvimulf  15809  dvcjbr  15811  dvcj  15812  dvrecap  15816  dvmptclx  15821  uhgrm  16331  wrdupgren  16349  upgrfnen  16351  wrdumgren  16359  umgrfnen  16361  upgr2wlkdc  16630  wlkres  16632