Theorem relres 5991

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

Step	Hyp	Ref	Expression
1		df-res 5659	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4189	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3982	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5665	. 2 ⊢ Rel (𝐵 × V)
5		relss 5754	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3454   ∩ cin 3903   ⊆ wss 3904   × cxp 5645   ↾ cres 5649  Rel wrel 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-in 3911  df-ss 3921  df-opab 5163  df-xp 5653  df-rel 5654  df-res 5659

This theorem is referenced by:  resindm  6016  relresdm1  6022  iss  6024  dfres2  6030  restidsing  6042  asymref  6103  poirr2  6111  cnvcnvres  6192  resco  6237  coeq0  6243  resssxp  6257  ressn  6272  dfpo2  6283  snres0  6285  funssres  6565  fnresdisj  6641  fnres  6648  fresaunres2  6736  fcnvres  6741  nfunsn  6906  dffv2  6962  fsnunfv  7171  eqfunresadj  7344  resfunexgALT  7929  elecres  8727  domss2  9108  fidomdm  9277  ttrclco  9673  cottrcl  9674  dmttrcl  9676  rnttrcl  9677  frmin  9707  frrlem16  9716  frr1  9717  dmct  10481  relexp0rel  15050  setsres  17214  pospo  18375  metustid  24614  ovoliunlem1  25564  dvres  25973  dvres2  25974  dvlog  26716  efopnlem2  26722  noetasuplem2  27798  noetainflem2  27802  h2hlm  31183  hlimcaui  31439  dfrdg2  36143  funpartfun  36293  bj-idreseq  37654  bj-idreseqb  37655  brres2  38772  br1cnvssrres  39084  refrelressn  39103  trrelressn  39166  dfeldisj2  39309  dfeldisj3  39310  dfeldisj4  39311  disjres  39343  antisymrelres  39365  antisymrelressn  39366  mapfzcons1  43298  diophrw  43340  eldioph2lem1  43341  eldioph2lem2  43342  undmrnresiss  44180  brfvrcld2  44268  relexpiidm  44280  limsupresuz  46277  liminfresuz  46358  funressnfv  47637  dfdfat2  47722  resinsn  49493  resinsnALT  49494  tposres0  49498  setrec2lem2  50315