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

Theorem fneq2i 5507
Description: Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.)
Hypothesis
Ref Expression
fneq2i.1  |-  A  =  B
Assertion
Ref Expression
fneq2i  |-  ( F  Fn  A  <->  F  Fn  B )

Proof of Theorem fneq2i
StepHypRef Expression
1 fneq2i.1 . 2  |-  A  =  B
2 fneq2 5502 . 2  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
31, 2ax-mp 8 1  |-  ( F  Fn  A  <->  F  Fn  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    Fn wfn 5416
This theorem is referenced by:  fnunsn  5519  fnsuppeq0  5920  tpos0  6476  dfixp  7032  ordtypelem4  7454  ser0f  11339  eqs1  11724  efcvgfsum  12651  prmrec  13253  xpscfn  13747  mulgfvi  14857  ovolunlem1  19354  volsup  19411  mtest  20281  mtestbdd  20282  pserulm  20299  pserdvlem2  20305  emcllem5  20799  esumfsup  24421  esumpcvgval  24429  esumcvg  24437  lgamgulm2  24781  lgamcvglem  24785  gamcvg2lem  24804  prodf1f  25181  faclimlem1  25318  wfrlem5  25482  frrlem5  25507  fullfunfnv  25707  mblfinlem  26151  ovoliunnfl  26155  voliunnfl  26157  bnj149  28964  bnj1312  29145
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2405  df-fn 5424
  Copyright terms: Public domain W3C validator