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

Theorem fvresi 6097
Description: The value of a restricted identity function. (Contributed by NM, 19-May-2004.)
Assertion
Ref Expression
fvresi

Proof of Theorem fvresi
StepHypRef Expression
1 fvres 5885 . 2
2 fvi 5930 . 2
31, 2eqtrd 2498 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818   cid 4795  |`cres 5006  `cfv 5593
This theorem is referenced by:  fninfp  6098  fndifnfp  6100  fnnfpeq0  6102  f1ocnvfv1  6182  f1ocnvfv2  6183  fcof1  6190  fcofo  6191  isoid  6225  weniso  6250  iordsmo  7047  fipreima  7846  infxpenc  8416  infxpencOLD  8421  dfac9  8537  ndxarg  14652  idfu2  15247  idfu1  15249  idfucl  15250  cofurid  15260  yonedainv  15550  idmhm  15975  idghm  16282  lactghmga  16429  symgga  16431  cayleylem2  16438  gsmsymgrfix  16453  gsmsymgreq  16457  pmtrfinv  16486  idlmhm  17687  evl1vard  18373  islinds2  18848  lindsind2  18854  madetsumid  18963  mdetunilem7  19120  txkgen  20153  ustuqtop3  20746  iducn  20786  nmoid  21249  dvid  22321  mvth  22393  fta1blem  22569  qaa  22719  idmot  23924  dfiop2  26672  idunop  26897  idcnop  26900  elunop2  26932  lnophm  26938  qqhre  27998  subfacp1lem4  28627  subfacp1lem5  28628  cvmliftlem5  28734  ghomsn  29028  rngunsnply  31122  idmgmhm  32476  funcestrcsetclem6  32651  funcestrcsetclem7  32652  funcestrcsetclem9  32654  funcsetcestrclem6  32666  funcsetcestrclem7  32667  funcsetcestrclem9  32669  funcrngcsetcALT  32807  funcringcsetcOLD2lem6  32849  funcringcsetcOLD2lem7  32850  funcringcsetcOLD2lem9  32852  funcringcsetclem6OLD  32872  funcringcsetclem7OLD  32873  funcringcsetclem9OLD  32875  dflinc2  33011  idlaut  35820  idldil  35838  ltrnid  35859  idltrn  35874  ltrnideq  35900  tendoidcl  36495  tendo1ne0  36554  cdleml7  36708  tendospid  36744  dvalveclem  36752
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-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
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-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  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-uni 4250  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-res 5016  df-iota 5556  df-fun 5595  df-fv 5601
  Copyright terms: Public domain W3C validator