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

Theorem fneq2i 5676
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 5670 . 2  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
31, 2ax-mp 5 1  |-  ( F  Fn  A  <->  F  Fn  B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1379    Fn wfn 5583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459  df-fn 5591
This theorem is referenced by:  fnunsn  5688  fnprb  6119  fnsuppeq0OLD  6122  fnsuppeq0  6928  tpos0  6985  dfixp  7471  ordtypelem4  7946  ser0f  12128  eqs1  12584  0csh0  12727  efcvgfsum  13683  prmrec  14299  xpscfn  14814  mulgfvi  15956  ovolunlem1  21671  volsup  21729  mtest  22561  mtestbdd  22562  pserulm  22579  pserdvlem2  22585  emcllem5  23085  tglnfn  23690  resf1o  27253  esumfsup  27744  esumpcvgval  27752  esumcvg  27760  lgamgulm2  28246  lgamcvglem  28250  gamcvg2lem  28269  prodf1f  28631  faclimlem1  28773  wfrlem5  28952  frrlem5  28996  fullfunfnv  29201  mblfinlem2  29657  ovoliunnfl  29661  voliunnfl  29663  bnj149  33030  bnj1312  33211
  Copyright terms: Public domain W3C validator