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

Theorem fneq1d 6019
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 6017 . 2 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
31, 2syl 17 1 (𝜑 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523   Fn wfn 5921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-fun 5928  df-fn 5929
This theorem is referenced by:  fneq12d  6021  f1o00  6209  f1oprswap  6218  f1ompt  6422  fmpt2d  6433  f1ocnvd  6926  offn  6950  offval2f  6951  offval2  6956  ofrfval2  6957  caofinvl  6966  suppsnop  7354  omxpenlem  8102  itunifn  9277  konigthlem  9428  seqof  12898  swrdlen  13468  mptfzshft  14554  fsumrev  14555  fprodrev  14751  prdsdsfn  16172  imasdsfn  16221  xpscfn  16266  cidfn  16387  comffn  16412  isoval  16472  invf1o  16476  isofn  16482  brssc  16521  cofucl  16595  estrchomfn  16822  funcestrcsetclem4  16830  funcsetcestrclem4  16845  1stfcl  16884  2ndfcl  16885  prfcl  16890  evlfcl  16909  curf1cl  16915  curfcl  16919  hofcl  16946  yonedainv  16968  grpinvf1o  17532  pmtrrn  17923  pmtrfrn  17924  srngf1o  18902  ofco2  20305  mat1dimscm  20329  neif  20952  fmf  21796  fncpn  23741  mdeg0  23875  tglnfn  25487  grpoinvf  27514  kbass2  29104  fnresin  29558  f1o3d  29559  f1od2  29627  pstmxmet  30068  prodindf  30213  ofcfn  30290  ofcfval2  30294  signstlen  30772  bnj941  30969  msubrn  31552  poimirlem4  33543  cnambfre  33588  sdclem2  33668  diafn  36640  dibfna  36760  dicfnN  36789  dihf11lem  36872  mapd1o  37254  hdmapfnN  37438  hgmapfnN  37497  hbtlem7  38012  fsovf1od  38627  ntrrn  38737  ntrf  38738  dssmapntrcls  38743  addrfn  38993  subrfn  38994  mulvfn  38995  fsumsermpt  40129  hoidmvlelem3  41132  smflimsuplem7  41353  rnghmresfn  42288  rhmresfn  42334  funcringcsetcALTV2lem4  42364  funcringcsetclem4ALTV  42387  rhmsubclem1  42411  rhmsubcALTVlem1  42429
  Copyright terms: Public domain W3C validator