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

Theorem fneq1d 5676
Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
fneq1d.1
Assertion
Ref Expression
fneq1d

Proof of Theorem fneq1d
StepHypRef Expression
1 fneq1d.1 . 2
2 fneq1 5674 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  Fnwfn 5588
This theorem is referenced by:  fneq12d  5678  f1o00  5853  f1oprswap  5860  f1ompt  6053  fmpt2d  6061  f1ocnvd  6524  offn  6551  offval2  6556  ofrfval2  6557  caofinvl  6567  suppsnop  6932  omxpenlem  7638  itunifn  8818  konigthlem  8964  seqof  12164  swrdlen  12650  mptfzshft  13593  fsumrev  13594  fprodrev  13781  prdsdsfn  14862  imasdsfn  14911  xpscfn  14956  cidfn  15076  comffn  15100  isoval  15159  invf1o  15163  brssc  15183  cofucl  15257  1stfcl  15466  2ndfcl  15467  prfcl  15472  evlfcl  15491  curf1cl  15497  curfcl  15501  hofcl  15528  yonedainv  15550  grpinvf1o  16108  pmtrrn  16482  pmtrfrn  16483  srngf1o  17503  ofco2  18953  mat1dimscm  18977  neif  19601  fmf  20446  fncpn  22336  mdeg0  22470  tglnfn  23934  grpoinvf  25242  kbass2  27036  fnresin  27470  f1o3d  27471  offval2f  27506  f1od2  27547  pstmxmet  27876  ofcfn  28099  ofcfval2  28103  signstlen  28524  msubrn  28889  cnambfre  30063  sdclem2  30235  hbtlem7  31074  addrfn  31381  subrfn  31382  mulvfn  31383  isofn  32567  estrchomfn  32641  funcestrcsetclem4  32649  funcsetcestrclem4  32664  rnghmresfn  32771  rhmresfn  32817  funcringcsetcOLD2lem4  32847  funcringcsetclem4OLD  32870  rhmsubclem1  32894  rhmsubcOLDlem1  32913  bnj941  33831  diafn  36761  dibfna  36881  dicfnN  36910  dihf11lem  36993  mapd1o  37375  hdmapfnN  37559  hgmapfnN  37618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-fun 5595  df-fn 5596
  Copyright terms: Public domain W3C validator