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

Theorem fneq2i 5505
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 5499 . 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 1369    Fn wfn 5412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2435  df-fn 5420
This theorem is referenced by:  fnunsn  5517  fnprb  5935  fnsuppeq0OLD  5938  fnsuppeq0  6716  tpos0  6774  dfixp  7264  ordtypelem4  7734  ser0f  11858  eqs1  12299  0csh0  12429  efcvgfsum  13370  prmrec  13982  xpscfn  14496  mulgfvi  15630  ovolunlem1  20979  volsup  21036  mtest  21868  mtestbdd  21869  pserulm  21886  pserdvlem2  21892  emcllem5  22392  tglnfn  22980  resf1o  26029  esumfsup  26518  esumpcvgval  26526  esumcvg  26534  lgamgulm2  27021  lgamcvglem  27025  gamcvg2lem  27044  prodf1f  27406  faclimlem1  27548  wfrlem5  27727  frrlem5  27771  fullfunfnv  27976  mblfinlem2  28427  ovoliunnfl  28431  voliunnfl  28433  bnj149  31866  bnj1312  32047
  Copyright terms: Public domain W3C validator