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

Theorem fneq1i 6514
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 6508 . 2 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
31, 2ax-mp 5 1 (𝐹 Fn 𝐴𝐺 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1539   Fn wfn 6413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-fun 6420  df-fn 6421
This theorem is referenced by:  fnunop  6531  mptfnf  6552  fnopabg  6554  f1oun  6719  f1oi  6737  f1osn  6739  ovid  7392  curry1  7915  curry2  7918  fsplitfpar  7930  frrlem11  8083  wfrlem5OLD  8115  wfrlem13OLD  8123  tfrlem10  8189  tfr1  8199  seqomlem2  8252  seqomlem3  8253  seqomlem4  8254  fnseqom  8256  unblem4  8999  r1fnon  9456  alephfnon  9752  alephfplem4  9794  alephfp  9795  cfsmolem  9957  infpssrlem3  9992  compssiso  10061  hsmexlem5  10117  axdclem2  10207  wunex2  10425  wuncval2  10434  om2uzrani  13600  om2uzf1oi  13601  uzrdglem  13605  uzrdgfni  13606  uzrdg0i  13607  hashkf  13974  dmaf  17680  cdaf  17681  prdsinvlem  18599  srg1zr  19680  pws1  19770  frlmphl  20898  ovolunlem1  24566  0plef  24741  0pledm  24742  itg1ge0  24755  itg1addlem4OLD  24769  mbfi1fseqlem5  24789  itg2addlem  24828  qaa  25388  ex-fpar  28727  0vfval  28869  xrge0pluscn  31792  bnj927  32649  bnj535  32770  fullfunfnv  34175  neibastop2lem  34476  fourierdlem42  43580  fcoreslem4  44447  rngcrescrhm  45531  rngcrescrhmALTV  45549
  Copyright terms: Public domain W3C validator