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

Theorem relres 5875
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 5560 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss2 4203 . . 3 (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
31, 2eqsstri 3998 . 2 (𝐴𝐵) ⊆ (𝐵 × V)
4 relxp 5566 . 2 Rel (𝐵 × V)
5 relss 5649 . 2 ((𝐴𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴𝐵)))
63, 4, 5mp2 9 1 Rel (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3492  cin 3932  wss 3933   × cxp 5546  cres 5550  Rel wrel 5553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-in 3940  df-ss 3949  df-opab 5120  df-xp 5554  df-rel 5555  df-res 5560
This theorem is referenced by:  iss  5896  dfres2  5902  restidsing  5915  asymref  5969  poirr2  5977  cnvcnvres  6055  resco  6096  coeq0  6101  ressn  6129  funssres  6391  fnresdisj  6460  fnres  6467  fresaunres2  6543  fcnvres  6549  nfunsn  6700  dffv2  6749  fsnunfv  6941  resfunexgALT  7638  domss2  8664  fidomdm  8789  dmct  9934  relexp0rel  14384  setsres  16513  pospo  17571  metustid  23091  ovoliunlem1  24030  dvres  24436  dvres2  24437  dvlog  25161  efopnlem2  25167  h2hlm  28684  hlimcaui  28940  funresdm1  30283  dfpo2  32888  eqfunresadj  32901  dfrdg2  32937  funpartfun  33301  bj-idreseq  34346  bj-idreseqb  34347  brres2  35410  elecres  35415  br1cnvssrres  35625  dfeldisj2  35831  dfeldisj3  35832  dfeldisj4  35833  mapfzcons1  39192  diophrw  39234  eldioph2lem1  39235  eldioph2lem2  39236  undmrnresiss  39842  brfvrcld2  39915  relexpiidm  39927  rp-imass  39995  limsupresuz  41860  liminfresuz  41941  funressnfv  43155  dfdfat2  43204  setrec2lem2  44725
  Copyright terms: Public domain W3C validator