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

Theorem relres 5855
Description: A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
relres Rel (𝐴𝐵)

Proof of Theorem relres
StepHypRef Expression
1 df-res 5540 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss2 4181 . . 3 (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
31, 2eqsstri 3977 . 2 (𝐴𝐵) ⊆ (𝐵 × V)
4 relxp 5546 . 2 Rel (𝐵 × V)
5 relss 5629 . 2 ((𝐴𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴𝐵)))
63, 4, 5mp2 9 1 Rel (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3471  cin 3909  wss 3910   × cxp 5526  cres 5530  Rel wrel 5533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-rab 3135  df-v 3473  df-in 3917  df-ss 3927  df-opab 5102  df-xp 5534  df-rel 5535  df-res 5540
This theorem is referenced by:  iss  5876  dfres2  5882  restidsing  5895  asymref  5949  poirr2  5957  cnvcnvres  6035  resco  6076  coeq0  6081  ressn  6109  funssres  6371  fnresdisj  6440  fnres  6447  fresaunres2  6523  fcnvres  6529  nfunsn  6680  dffv2  6729  fsnunfv  6922  resfunexgALT  7624  domss2  8652  fidomdm  8777  dmct  9923  relexp0rel  14375  setsres  16504  pospo  17562  metustid  23140  ovoliunlem1  24085  dvres  24493  dvres2  24494  dvlog  25221  efopnlem2  25227  h2hlm  28742  hlimcaui  28998  funresdm1  30342  dfpo2  32999  eqfunresadj  33012  dfrdg2  33048  funpartfun  33412  bj-idreseq  34472  bj-idreseqb  34473  brres2  35575  elecres  35580  br1cnvssrres  35791  dfeldisj2  35997  dfeldisj3  35998  dfeldisj4  35999  mapfzcons1  39469  diophrw  39511  eldioph2lem1  39512  eldioph2lem2  39513  undmrnresiss  40115  brfvrcld2  40204  relexpiidm  40216  rp-imass  40284  limsupresuz  42168  liminfresuz  42249  funressnfv  43458  dfdfat2  43507  setrec2lem2  45035
  Copyright terms: Public domain W3C validator