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

Theorem fneq2i 6445
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 6439 . 2 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
31, 2ax-mp 5 1 (𝐹 Fn 𝐴𝐹 Fn 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528   Fn wfn 6344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-fn 6352
This theorem is referenced by:  fnunsn  6458  fnprb  6963  fntpb  6964  fnsuppeq0  7849  tpos0  7913  wfrlem5  7950  dfixp  8452  ordtypelem4  8974  ser0f  13413  0csh0  14145  s3fn  14263  prodf1f  15238  efcvgfsum  15429  prmrec  16248  fnpr2o  16820  0ssc  17097  0subcat  17098  mulgfvi  18170  ovolunlem1  24027  volsup  24086  mtest  24921  mtestbdd  24922  pserulm  24939  pserdvlem2  24945  emcllem5  25505  lgamgulm2  25541  lgamcvglem  25545  gamcvg2lem  25564  tglnfn  26261  crctcshlem4  27526  fsuppcurry1  30388  fsuppcurry2  30389  resf1o  30393  s2rn  30548  s3rn  30550  cycpmfvlem  30682  cycpmfv3  30685  esumfsup  31229  esumpcvgval  31237  esumcvg  31245  esumsup  31248  bnj149  32047  bnj1312  32228  faclimlem1  32873  fullfunfnv  33305  knoppcnlem8  33737  knoppcnlem11  33740  mblfinlem2  34812  ovoliunnfl  34816  voliunnfl  34818  subsaliuncl  42522
  Copyright terms: Public domain W3C validator