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

Theorem fneq2i 5625
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 5619 . 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 5532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2415  df-fn 5540
This theorem is referenced by:  fnunsn  5637  fnprb  6075  fnsuppeq0  6891  tpos0  6951  wfrlem5  6988  dfixp  7472  ordtypelem4  7982  ser0f  12209  0csh0  12834  prodf1f  13884  efcvgfsum  14076  prmrec  14802  xpscfn  15401  0ssc  15678  0subcat  15679  mulgfvi  16698  ovolunlem1  22385  volsup  22444  mtest  23294  mtestbdd  23295  pserulm  23312  pserdvlem2  23318  emcllem5  23860  lgamgulm2  23896  lgamcvglem  23900  gamcvg2lem  23919  tglnfn  24527  resf1o  28258  esumfsup  28836  esumpcvgval  28844  esumcvg  28852  esumsup  28855  bnj149  29631  bnj1312  29812  faclimlem1  30323  frrlem5  30462  fullfunfnv  30655  mblfinlem2  31879  ovoliunnfl  31883  voliunnfl  31885
  Copyright terms: Public domain W3C validator