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

Theorem relres 5329
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 5036 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × V))
2 inss2 3791 . . 3 (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
31, 2eqsstri 3593 . 2 (𝐴𝐵) ⊆ (𝐵 × V)
4 relxp 5135 . 2 Rel (𝐵 × V)
5 relss 5115 . 2 ((𝐴𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴𝐵)))
63, 4, 5mp2 9 1 Rel (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  Vcvv 3168  cin 3534  wss 3535   × cxp 5022  cres 5026  Rel wrel 5029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-in 3542  df-ss 3549  df-opab 4634  df-xp 5030  df-rel 5031  df-res 5036
This theorem is referenced by:  elres  5338  iss  5350  dfres2  5355  restidsing  5360  restidsingOLD  5361  issref  5411  asymref  5414  poirr2  5422  cnvcnvres  5498  resco  5538  coeq0  5543  ressn  5570  funssres  5826  fnresdisj  5897  fnres  5903  fresaunres2  5970  fcnvres  5976  nfunsn  6116  dffv2  6162  fsnunfv  6332  resiexg  6967  resfunexgALT  6995  domss2  7977  fidomdm  8101  relexp0rel  13567  setsres  15671  pospo  16738  metustid  22106  ovoliunlem1  22990  dvres  23394  dvres2  23395  dvlog  24110  efopnlem2  24116  h2hlm  27023  hlimcaui  27279  dmct  28679  dfpo2  30700  dfrdg2  30747  funpartfun  31022  mapfzcons1  36097  diophrw  36139  eldioph2lem1  36140  eldioph2lem2  36141  undmrnresiss  36728  rtrclexi  36746  brfvrcld2  36802  relexpiidm  36814  rp-imass  36884  idhe  36900  funressnfv  39657  dfdfat2  39661
  Copyright terms: Public domain W3C validator