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

Theorem fneq2i 6163
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 6157 . 2 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
31, 2ax-mp 5 1 (𝐹 Fn 𝐴𝐹 Fn 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1652   Fn wfn 6062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2757  df-fn 6070
This theorem is referenced by:  fnunsn  6175  fnprb  6664  fntpb  6665  fnsuppeq0  7525  tpos0  7584  wfrlem5  7622  dfixp  8114  ordtypelem4  8632  ser0f  13060  0csh0  13817  s3fn  13941  prodf1f  14908  efcvgfsum  15099  prmrec  15906  xpscfn  16486  0ssc  16763  0subcat  16764  mulgfvi  17813  ovolunlem1  23554  volsup  23613  mtest  24448  mtestbdd  24449  pserulm  24466  pserdvlem2  24472  emcllem5  25016  lgamgulm2  25052  lgamcvglem  25056  gamcvg2lem  25075  tglnfn  25732  crctcshlem4  27003  resf1o  29888  esumfsup  30513  esumpcvgval  30521  esumcvg  30529  esumsup  30532  bnj149  31324  bnj1312  31505  faclimlem1  32005  frrlem5  32159  fullfunfnv  32428  knoppcnlem8  32860  knoppcnlem11  32863  mblfinlem2  33803  ovoliunnfl  33807  voliunnfl  33809  subsaliuncl  41145
  Copyright terms: Public domain W3C validator