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

Theorem fneq1i 6600
Description: Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
fneq1i.1 𝐹 = 𝐺
Assertion
Ref Expression
fneq1i (𝐹 Fn 𝐴𝐺 Fn 𝐴)

Proof of Theorem fneq1i
StepHypRef Expression
1 fneq1i.1 . 2 𝐹 = 𝐺
2 fneq1 6594 . 2 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
31, 2ax-mp 5 1 (𝐹 Fn 𝐴𝐺 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542   Fn wfn 6492
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-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-fun 6499  df-fn 6500
This theorem is referenced by:  fnunop  6617  mptfnf  6637  fnopabg  6639  f1oun  6804  f1oi  6823  f1osn  6825  ovid  7497  curry1  8037  curry2  8040  fsplitfpar  8051  frrlem11  8228  wfrlem5OLD  8260  wfrlem13OLD  8268  tfrlem10  8334  tfr1  8344  seqomlem2  8398  seqomlem3  8399  seqomlem4  8400  fnseqom  8402  unblem4  9245  r1fnon  9708  alephfnon  10006  alephfplem4  10048  alephfp  10049  cfsmolem  10211  infpssrlem3  10246  compssiso  10315  hsmexlem5  10371  axdclem2  10461  wunex2  10679  wuncval2  10688  om2uzrani  13863  om2uzf1oi  13864  uzrdglem  13868  uzrdgfni  13869  uzrdg0i  13870  hashkf  14238  dmaf  17940  cdaf  17941  prdsinvlem  18861  srg1zr  19951  pws1  20045  frlmphl  21203  ovolunlem1  24877  0plef  25052  0pledm  25053  itg1ge0  25066  itg1addlem4OLD  25080  mbfi1fseqlem5  25100  itg2addlem  25139  qaa  25699  ex-fpar  29448  0vfval  29590  xrge0pluscn  32578  bnj927  33438  bnj535  33559  fullfunfnv  34577  neibastop2lem  34878  fnmptif  43581  fourierdlem42  44476  fcoreslem4  45386  rngcrescrhm  46469  rngcrescrhmALTV  46487
  Copyright terms: Public domain W3C validator