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

Theorem fneq2i 6596
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 6590 . 2 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
31, 2ax-mp 5 1 (𝐹 Fn 𝐴𝐹 Fn 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542   Fn wfn 6487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2730  df-fn 6495
This theorem is referenced by:  fnunop  6612  fnprb  7153  fntpb  7154  fnsuppeq0  8091  tpos0  8155  wfrlem5OLD  8227  dfixp  8771  ordtypelem4  9391  ser0f  13890  0csh0  14613  s3fn  14732  prodf1f  15712  efcvgfsum  15903  prmrec  16729  fnpr2o  17374  0ssc  17658  0subcat  17659  mulgfvi  18812  ovolunlem1  24783  volsup  24842  mtest  25685  mtestbdd  25686  pserulm  25703  pserdvlem2  25709  emcllem5  26271  lgamgulm2  26307  lgamcvglem  26311  gamcvg2lem  26330  tglnfn  27275  crctcshlem4  28551  fsuppcurry1  31424  fsuppcurry2  31425  resf1o  31429  s2rn  31582  s3rn  31584  cycpmfvlem  31743  cycpmfv3  31746  esumfsup  32430  esumpcvgval  32438  esumcvg  32446  esumsup  32449  bnj149  33248  bnj1312  33431  faclimlem1  34094  fullfunfnv  34417  knoppcnlem8  34849  knoppcnlem11  34852  mblfinlem2  36002  ovoliunnfl  36006  voliunnfl  36008  subsaliuncl  44307  fcores  45001
  Copyright terms: Public domain W3C validator