Theorem fneq2d 5677

Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
fneq2d.1

Assertion

Ref	Expression
fneq2d

Proof of Theorem fneq2d

Step	Hyp	Ref	Expression
1		fneq2d.1	. 2
2		fneq2 5675	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  Fnwfn 5588

This theorem is referenced by:  fneq12d  5678  fnprb  6129  undifixp  7525  brwdom2  8020  dfac3  8523  ac7g  8875  ccatlid  12603  ccatrid  12604  ccatass  12605  swrdid  12652  ccatswrd  12681  swrdccat2  12683  swrdswrd  12685  swrdccatin2  12712  swrdccatin12  12716  revccat  12740  revrev  12741  repsdf2  12750  0csh0  12764  cshco  12802  seqshft  12918  invf  15162  sscfn1  15186  sscfn2  15187  isssc  15189  fuchom  15330  mulgfval  16143  symgplusg  16414  subrgascl  18163  frlmsslss2  18805  frlmsslss2OLD  18806  m1detdiag  19099  ptval  20071  xpsdsfn2  20881  pl1cn  27937  ofccat  28497  signsvtn0  28527  signstres  28532  uzmptshftfval  31251  estrchomfeqhom  32642  srhmsubc  32884  srhmsubcOLD  32903  bnj927  33827  dibfnN  36883  dihintcl  37071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449  df-fn 5596