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

Theorem fneq2i 5689
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 5683 . 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 187    = wceq 1437    Fn wfn 5596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2421  df-fn 5604
This theorem is referenced by:  fnunsn  5701  fnprb  6138  fnsuppeq0  6954  tpos0  7011  wfrlem5  7048  dfixp  7532  ordtypelem4  8036  ser0f  12263  0csh0  12880  prodf1f  13926  efcvgfsum  14118  prmrec  14829  xpscfn  15416  0ssc  15693  0subcat  15694  mulgfvi  16713  ovolunlem1  22328  volsup  22386  mtest  23224  mtestbdd  23225  pserulm  23242  pserdvlem2  23248  emcllem5  23790  lgamgulm2  23826  lgamcvglem  23830  gamcvg2lem  23849  tglnfn  24452  resf1o  28158  esumfsup  28730  esumpcvgval  28738  esumcvg  28746  esumsup  28749  bnj149  29474  bnj1312  29655  faclimlem1  30166  frrlem5  30305  fullfunfnv  30498  mblfinlem2  31682  ovoliunnfl  31686  voliunnfl  31688
  Copyright terms: Public domain W3C validator