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

Theorem fneq2i 5569
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 5564 . 2  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
31, 2ax-mp 5 1  |-  ( F  Fn  A  <->  F  Fn  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1653    Fn wfn 5478
This theorem is referenced by:  fnunsn  5581  fnsuppeq0  5982  tpos0  6538  dfixp  7094  ordtypelem4  7519  ser0f  11407  eqs1  11792  efcvgfsum  12719  prmrec  13321  xpscfn  13815  mulgfvi  14925  ovolunlem1  19424  volsup  19481  mtest  20351  mtestbdd  20352  pserulm  20369  pserdvlem2  20375  emcllem5  20869  esumfsup  24491  esumpcvgval  24499  esumcvg  24507  lgamgulm2  24851  lgamcvglem  24855  gamcvg2lem  24874  prodf1f  25251  faclimlem1  25393  wfrlem5  25573  frrlem5  25617  fullfunfnv  25822  mblfinlem2  26280  ovoliunnfl  26284  voliunnfl  26286  bnj149  29344  bnj1312  29525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-11 1763  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2435  df-fn 5486
  Copyright terms: Public domain W3C validator