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

Theorem fneq2i 6595
Description: Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.)
Hypothesis
Ref Expression
fneq2i.1 𝐴 = 𝐵
Assertion
Ref Expression
fneq2i (𝐹 Fn 𝐴𝐹 Fn 𝐵)

Proof of Theorem fneq2i
StepHypRef Expression
1 fneq2i.1 . 2 𝐴 = 𝐵
2 fneq2 6589 . 2 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
31, 2ax-mp 5 1 (𝐹 Fn 𝐴𝐹 Fn 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1541   Fn wfn 6486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2729  df-fn 6494
This theorem is referenced by:  fnunop  6611  fnprb  7152  fntpb  7153  fnsuppeq0  8090  tpos0  8154  wfrlem5OLD  8226  dfixp  8770  ordtypelem4  9390  ser0f  13889  0csh0  14612  s3fn  14731  prodf1f  15711  efcvgfsum  15902  prmrec  16728  fnpr2o  17373  0ssc  17657  0subcat  17658  mulgfvi  18811  ovolunlem1  24783  volsup  24842  mtest  25685  mtestbdd  25686  pserulm  25703  pserdvlem2  25709  emcllem5  26271  lgamgulm2  26307  lgamcvglem  26311  gamcvg2lem  26330  tglnfn  27287  crctcshlem4  28563  fsuppcurry1  31436  fsuppcurry2  31437  resf1o  31441  s2rn  31594  s3rn  31596  cycpmfvlem  31755  cycpmfv3  31758  esumfsup  32442  esumpcvgval  32450  esumcvg  32458  esumsup  32461  bnj149  33260  bnj1312  33443  faclimlem1  34106  fullfunfnv  34426  knoppcnlem8  34858  knoppcnlem11  34861  mblfinlem2  36011  ovoliunnfl  36015  voliunnfl  36017  subsaliuncl  44352  fcores  45050
  Copyright terms: Public domain W3C validator