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

Theorem fneq1i 6433
 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 6427 . 2 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
31, 2ax-mp 5 1 (𝐹 Fn 𝐴𝐺 Fn 𝐴)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   = wceq 1538   Fn wfn 6333 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3141  df-v 3481  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-br 5050  df-opab 5112  df-rel 5545  df-cnv 5546  df-co 5547  df-dm 5548  df-fun 6340  df-fn 6341 This theorem is referenced by:  fnunsn  6447  mptfnf  6466  fnopabg  6468  f1oun  6617  f1oi  6635  f1osn  6637  ovid  7275  curry1  7784  curry2  7787  fsplitfpar  7799  wfrlem5  7944  wfrlem13  7952  tfrlem10  8008  tfr1  8018  seqomlem2  8072  seqomlem3  8073  seqomlem4  8074  fnseqom  8076  unblem4  8759  r1fnon  9182  alephfnon  9478  alephfplem4  9520  alephfp  9521  cfsmolem  9679  infpssrlem3  9714  compssiso  9783  hsmexlem5  9839  axdclem2  9929  wunex2  10147  wuncval2  10156  om2uzrani  13315  om2uzf1oi  13316  uzrdglem  13320  uzrdgfni  13321  uzrdg0i  13322  hashkf  13688  dmaf  17300  cdaf  17301  prdsinvlem  18199  srg1zr  19270  pws1  19357  frlmphl  20913  ovolunlem1  24092  0plef  24267  0pledm  24268  itg1ge0  24281  itg1addlem4  24294  mbfi1fseqlem5  24314  itg2addlem  24353  qaa  24910  ex-fpar  28238  0vfval  28380  xrge0pluscn  31203  bnj927  32060  bnj535  32182  frrlem11  33153  fullfunfnv  33427  neibastop2lem  33728  fourierdlem42  42648  rngcrescrhm  44566  rngcrescrhmALTV  44584
 Copyright terms: Public domain W3C validator