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

Theorem relres 6015
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 5694 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss2 4231 . . 3 (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
31, 2eqsstri 4014 . 2 (𝐴𝐵) ⊆ (𝐵 × V)
4 relxp 5700 . 2 Rel (𝐵 × V)
5 relss 5787 . 2 ((𝐴𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴𝐵)))
63, 4, 5mp2 9 1 Rel (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3462  cin 3946  wss 3947   × cxp 5680  cres 5684  Rel wrel 5687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-in 3954  df-ss 3964  df-opab 5216  df-xp 5688  df-rel 5689  df-res 5694
This theorem is referenced by:  relresdm1  6042  iss  6044  dfres2  6050  restidsing  6062  asymref  6128  poirr2  6136  cnvcnvres  6216  resco  6261  coeq0  6266  resssxp  6281  ressn  6296  dfpo2  6307  snres0  6309  funssres  6603  fnresdisj  6681  fnres  6688  fresaunres2  6774  fcnvres  6779  nfunsn  6943  dffv2  6997  fsnunfv  7201  eqfunresadj  7372  resfunexgALT  7961  domss2  9174  fidomdm  9376  ttrclco  9761  cottrcl  9762  dmttrcl  9764  rnttrcl  9765  frmin  9792  frrlem16  9801  frr1  9802  dmct  10567  relexp0rel  15042  setsres  17180  pospo  18370  metustid  24554  ovoliunlem1  25522  dvres  25931  dvres2  25932  dvlog  26678  efopnlem2  26684  noetasuplem2  27764  noetainflem2  27768  h2hlm  30913  hlimcaui  31169  dfrdg2  35619  funpartfun  35767  bj-idreseq  36869  bj-idreseqb  36870  brres2  37966  elecres  37975  br1cnvssrres  38203  refrelressn  38222  trrelressn  38281  dfeldisj2  38416  dfeldisj3  38417  dfeldisj4  38418  disjres  38442  antisymrelres  38461  antisymrelressn  38462  mapfzcons1  42374  diophrw  42416  eldioph2lem1  42417  eldioph2lem2  42418  undmrnresiss  43271  brfvrcld2  43359  relexpiidm  43371  limsupresuz  45324  liminfresuz  45405  funressnfv  46658  dfdfat2  46741  setrec2lem2  48440
  Copyright terms: Public domain W3C validator