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

Theorem fneq1d 6439
Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
fneq1d.1 (𝜑𝐹 = 𝐺)
Assertion
Ref Expression
fneq1d (𝜑 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))

Proof of Theorem fneq1d
StepHypRef Expression
1 fneq1d.1 . 2 (𝜑𝐹 = 𝐺)
2 fneq1 6437 . 2 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
31, 2syl 17 1 (𝜑 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528   Fn wfn 6343
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-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-fun 6350  df-fn 6351
This theorem is referenced by:  fneq12d  6441  f1o00  6642  f1oprswap  6651  f1ompt  6867  fmpt2d  6879  f1ocnvd  7385  offn  7409  offval2f  7410  offval2  7415  ofrfval2  7416  caofinvl  7425  fsplitfpar  7803  omxpenlem  8606  itunifn  9827  konigthlem  9978  seqof  13415  swrdlen  13997  mptfzshft  15121  fprodrev  15319  prdsdsfn  16726  imasdsfn  16775  cidfn  16938  comffn  16963  isoval  17023  invf1o  17027  isofn  17033  brssc  17072  cofucl  17146  estrchomfn  17373  funcestrcsetclem4  17381  funcsetcestrclem4  17396  1stfcl  17435  2ndfcl  17436  prfcl  17441  evlfcl  17460  curf1cl  17466  curfcl  17470  hofcl  17497  yonedainv  17519  grpinvf1o  18107  pmtrrn  18514  pmtrfrn  18515  srngf1o  19554  ofco2  20988  mat1dimscm  21012  neif  21636  fmf  22481  fncpn  24457  mdeg0  24591  tglnfn  26260  grpoinvf  28236  kbass2  29821  fnresin  30299  f1o3d  30300  suppovss  30354  f1od2  30383  frlmdim  30908  pstmxmet  31036  prodindf  31181  ofcfn  31258  ofcfval2  31262  signstlen  31736  bnj941  31943  satfn  32499  msubrn  32673  poimirlem4  34777  cnambfre  34821  sdclem2  34898  diafn  38050  dibfna  38170  dicfnN  38199  dihf11lem  38282  mapd1o  38664  hdmapfnN  38845  hgmapfnN  38904  hbtlem7  39603  fsovf1od  40240  ntrrn  40350  ntrf  40351  dssmapntrcls  40356  addrfn  40681  subrfn  40682  mulvfn  40683  fsumsermpt  41736  hoidmvlelem3  42756  smflimsuplem7  42977  smndex1n0mnd  44012  rnghmresfn  44162  rhmresfn  44208  funcringcsetcALTV2lem4  44238  funcringcsetclem4ALTV  44261  rhmsubclem1  44285  rhmsubcALTVlem1  44303
  Copyright terms: Public domain W3C validator