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

Theorem fneq2i 5444
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 5439 . 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 176    = wceq 1647    Fn wfn 5353
This theorem is referenced by:  fnunsn  5456  fnsuppeq0  5853  tpos0  6406  dfixp  6962  ordtypelem4  7383  ser0f  11263  eqs1  11648  efcvgfsum  12575  prmrec  13177  xpscfn  13671  mulgfvi  14781  ovolunlem1  19071  volsup  19128  mtest  19998  mtestbdd  19999  pserulm  20016  pserdvlem2  20022  emcllem5  20516  esumfsup  24046  esumpcvgval  24054  esumcvg  24062  lgamgulm2  24389  lgamcvglem  24393  gamcvg2lem  24412  prodf1f  24789  faclimlem1  24922  wfrlem5  25086  frrlem5  25111  fullfunfnv  25311  ovoliunnfl  25756  voliunnfl  25758  bnj149  28659  bnj1312  28840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-cleq 2359  df-fn 5361
  Copyright terms: Public domain W3C validator