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

Theorem fneq1d 6443
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 6441 . 2 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
31, 2syl 17 1 (𝜑 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530   Fn wfn 6347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-br 5064  df-opab 5126  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-fun 6354  df-fn 6355
This theorem is referenced by:  fneq12d  6445  f1o00  6646  f1oprswap  6655  f1ompt  6871  fmpt2d  6883  f1ocnvd  7386  offn  7410  offval2f  7411  offval2  7416  ofrfval2  7417  caofinvl  7426  fsplitfpar  7805  omxpenlem  8607  itunifn  9828  konigthlem  9979  seqof  13417  swrdlen  13999  mptfzshft  15123  fprodrev  15321  prdsdsfn  16728  imasdsfn  16777  cidfn  16940  comffn  16965  isoval  17025  invf1o  17029  isofn  17035  brssc  17074  cofucl  17148  estrchomfn  17375  funcestrcsetclem4  17383  funcsetcestrclem4  17398  1stfcl  17437  2ndfcl  17438  prfcl  17443  evlfcl  17462  curf1cl  17468  curfcl  17472  hofcl  17499  yonedainv  17521  grpinvf1o  18099  pmtrrn  18505  pmtrfrn  18506  srngf1o  19545  ofco2  20976  mat1dimscm  21000  neif  21624  fmf  22469  fncpn  24445  mdeg0  24579  tglnfn  26247  grpoinvf  28223  kbass2  29808  fnresin  30286  f1o3d  30287  suppovss  30341  f1od2  30370  frlmdim  30895  pstmxmet  31023  prodindf  31168  ofcfn  31245  ofcfval2  31249  signstlen  31723  bnj941  31930  satfn  32486  msubrn  32660  poimirlem4  34763  cnambfre  34807  sdclem2  34885  diafn  38037  dibfna  38157  dicfnN  38186  dihf11lem  38269  mapd1o  38651  hdmapfnN  38832  hgmapfnN  38891  hbtlem7  39590  fsovf1od  40227  ntrrn  40337  ntrf  40338  dssmapntrcls  40343  addrfn  40669  subrfn  40670  mulvfn  40671  fsumsermpt  41725  hoidmvlelem3  42745  smflimsuplem7  42966  rnghmresfn  44066  rhmresfn  44112  funcringcsetcALTV2lem4  44142  funcringcsetclem4ALTV  44165  rhmsubclem1  44189  rhmsubcALTVlem1  44207
  Copyright terms: Public domain W3C validator