Theorem feq2d 5524

Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
feq2d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
feq2d	|- ( ph -> ( F : A --> C <-> F : B --> C ) )

Proof of Theorem feq2d

Step	Hyp	Ref	Expression
1		feq2d.1	. 2 |- ( ph -> A = B )
2		feq2 5520	. 2 |- ( A = B -> ( F : A --> C <-> F : B --> C ) )
3	1, 2	syl 14	1 |- ( ph -> ( F : A --> C <-> F : B --> C ) )

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  6565  qliftf  6899  elpm2r  6945  casef  7434  fseq1p1m1  10517  fseq1m1p1  10518  seqf  10921  seqf2  10925  seqf1og  10978  iswrdinn0  11330  wrdf  11331  iswrdiz  11332  wrdffz  11346  ffz0iswrdnn0  11352  wrdnval  11356  ccatalpha  11402  swrdf  11448  swrdwrdsymbg  11457  cats1un  11514  s2dmg  11583  intopsn  13745  resmhm  13852  gzsumwsubmcl  13859  gzsumwmhm  13861  isghm  14104  resghm  14121  gzsumsplit0  14237  gsumvalfi  14241  gzsumgsum  14244  gsummptfidmsplit  14253  psrelbasfi  15189  lmtopcnp  15493  ellimc3apf  15903  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dviaddf  15948  dvimulf  15949  dvcjbr  15951  dvcj  15952  dvrecap  15956  dvmptclx  15961  uhgrm  16541  wrdupgren  16559  upgrfnen  16561  wrdumgren  16569  umgrfnen  16571  upgr2wlkdc  16840  wlkres  16842