MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fneq2d Unicode version

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
StepHypRef Expression
1 fneq2d.1 . 2
2 fneq2 5675 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator