Theorem feq2d 4557

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 4552	. 2 |- (A = B -> (F:A-->C <-> F:B-->C))
3	1, 2	syl 12	1 |- (ph -> (F:A-->C <-> F:B-->C))

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298  -->wf 3994

This theorem is referenced by:  ffdm 4578  ac6sfilem3 5508  ismet 9075  dfms2 9076  ismsg 9077  msflem 9080  metreslem 9099  metcnpf 9161  metcnf 9162  metcnconst 9163  metdnsconst 9179  metcn4 9249  isgrp 9321  isring 9465  ringi 9466  vci 9499  isvclem 9528  vcoprnelem 9529  isnvlem 9561  nvi 9565  nvcnf 9659  nvcnpf 9660  lnoval 9752  nmofval 9764  ajfval 9809  elghomlem1 10193  tx1cn 10223  tx2cn 10224  filmapf 10307  fbfgfmeq 10315  flimff 10317  feq12d 13587  vecval3b 14795  istopx 14918  conttnf 14944  conttnf2 14945  cnpfillim4 14947  ismgra 15057  algi 15074  isfuna 15182  cnsubsp 15426  fmufil 15599  flimfbas 15601  fcluscnp 15618  fclusff 15623  filnet 15645  acdc5g 15752  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  fsumltisum 15824  fsumleisum 15827  trirn 15834  cnres 15889  bfp 16009  rrnmet 16016  isgrpda 16033  isringd 16097  rnghomval 16118

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877  df-fn 4009  df-f 4010

Copyright terms: Public domain