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

Theorem fneq2i 5339
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 5334 . 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 1623    Fn wfn 5250
This theorem is referenced by:  fnunsn  5351  fnsuppeq0  5733  tpos0  6264  dfixp  6819  ordtypelem4  7236  ser0f  11099  eqs1  11447  efcvgfsum  12367  prmrec  12969  xpscfn  13461  mulgfvi  14571  ovolunlem1  18856  volsup  18913  mtest  19781  pserulm  19798  pserdvlem2  19804  emcllem5  20293  esumpcvgval  23446  esumcvg  23454  wfrlem5  24260  frrlem5  24285  fullfunfnv  24484  repcpwti  25161  bnj149  28907  bnj1312  29088
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276  df-fn 5258
  Copyright terms: Public domain W3C validator