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

Theorem fneq2i 5625
 Description: Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.)
Hypothesis
Ref Expression
fneq2i.1
Assertion
Ref Expression
fneq2i

Proof of Theorem fneq2i
StepHypRef Expression
1 fneq2i.1 . 2
2 fneq2 5619 . 2
31, 2ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:   wb 187   wceq 1437   wfn 5532 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2402 This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2415  df-fn 5540 This theorem is referenced by:  fnunsn  5637  fnprb  6075  fnsuppeq0  6891  tpos0  6951  wfrlem5  6988  dfixp  7472  ordtypelem4  7982  ser0f  12209  0csh0  12834  prodf1f  13884  efcvgfsum  14076  prmrec  14802  xpscfn  15401  0ssc  15678  0subcat  15679  mulgfvi  16698  ovolunlem1  22385  volsup  22444  mtest  23294  mtestbdd  23295  pserulm  23312  pserdvlem2  23318  emcllem5  23860  lgamgulm2  23896  lgamcvglem  23900  gamcvg2lem  23919  tglnfn  24527  resf1o  28258  esumfsup  28836  esumpcvgval  28844  esumcvg  28852  esumsup  28855  bnj149  29631  bnj1312  29812  faclimlem1  30323  frrlem5  30462  fullfunfnv  30655  mblfinlem2  31879  ovoliunnfl  31883  voliunnfl  31885
 Copyright terms: Public domain W3C validator