Theorem feq2d 5464

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

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

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 5324  df-f 5325

This theorem is referenced by:  feq12d  5466  ffdm  5499  fsng  5813  issmo2  6446  qliftf  6780  elpm2r  6826  casef  7271  fseq1p1m1  10307  fseq1m1p1  10308  seqf  10703  seqf2  10707  seqf1og  10760  iswrdinn0  11094  wrdf  11095  iswrdiz  11096  wrdffz  11110  ffz0iswrdnn0  11116  wrdnval  11120  ccatalpha  11166  swrdf  11208  swrdwrdsymbg  11217  cats1un  11274  s2dmg  11343  intopsn  13421  gsumprval  13453  resmhm  13541  gsumwsubmcl  13550  gsumwmhm  13552  isghm  13801  resghm  13818  psrelbasfi  14661  lmtopcnp  14945  ellimc3apf  15355  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dviaddf  15400  dvimulf  15401  dvcjbr  15403  dvcj  15404  dvrecap  15408  dvmptclx  15413  uhgrm  15899  wrdupgren  15917  upgrfnen  15919  wrdumgren  15927  umgrfnen  15929  upgr2wlkdc  16147  wlkres  16149