Theorem fneq2i 5681

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

Step	Hyp	Ref	Expression
1		fneq2i.1	. 2
2		fneq2 5675	. 2
3	1, 2	ax-mp 5	1

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

This theorem is referenced by:  fnunsn  5693  fnprb  6129  fnsuppeq0OLD  6132  fnsuppeq0  6947  tpos0  7004  dfixp  7491  ordtypelem4  7967  ser0f  12160  eqs1  12621  0csh0  12764  prodf1f  13701  efcvgfsum  13821  prmrec  14440  xpscfn  14956  0ssc  15206  0subcat  15207  mulgfvi  16146  ovolunlem1  21908  volsup  21966  mtest  22799  mtestbdd  22800  pserulm  22817  pserdvlem2  22823  emcllem5  23329  tglnfn  23934  resf1o  27553  esumfsup  28076  esumpcvgval  28084  esumcvg  28092  lgamgulm2  28578  lgamcvglem  28582  gamcvg2lem  28601  faclimlem1  29168  wfrlem5  29347  frrlem5  29391  fullfunfnv  29596  mblfinlem2  30052  ovoliunnfl  30056  voliunnfl  30058  bnj149  33933  bnj1312  34114

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