Theorem relres 6004

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 5673	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4190	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3983	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5679	. 2 ⊢ Rel (𝐵 × V)
5		relss 5768	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3455   ∩ cin 3904   ⊆ wss 3905   × cxp 5659   ↾ cres 5663  Rel wrel 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3912  df-ss 3922  df-opab 5174  df-xp 5667  df-rel 5668  df-res 5673

This theorem is referenced by:  resindm  6029  relresdm1  6035  iss  6037  dfres2  6043  restidsing  6055  asymref  6116  poirr2  6124  cnvcnvres  6206  resco  6251  coeq0  6257  resssxp  6271  ressn  6286  dfpo2  6297  snres0  6299  funssres  6580  fnresdisj  6655  fnres  6662  fresaunres2  6750  fcnvres  6755  nfunsn  6920  dffv2  6976  fsnunfv  7185  eqfunresadj  7358  resfunexgALT  7941  elecres  8739  domss2  9120  fidomdm  9287  ttrclco  9683  cottrcl  9684  dmttrcl  9686  rnttrcl  9687  frmin  9717  frrlem16  9726  frr1  9727  dmct  10503  relexp0rel  15070  setsres  17233  pospo  18394  metustid  24711  ovoliunlem1  25661  dvres  26070  dvres2  26071  dvlog  26816  efopnlem2  26822  noetasuplem2  27898  noetainflem2  27902  h2hlm  31332  hlimcaui  31588  dfrdg2  36285  funpartfun  36435  bj-idreseq  37826  bj-idreseqb  37827  brres2  38942  br1cnvssrres  39254  refrelressn  39273  trrelressn  39336  dfeldisj2  39479  dfeldisj3  39480  dfeldisj4  39481  disjres  39513  antisymrelres  39535  antisymrelressn  39536  mapfzcons1  43468  diophrw  43510  eldioph2lem1  43511  eldioph2lem2  43512  undmrnresiss  44350  brfvrcld2  44438  relexpiidm  44450  limsupresuz  46437  liminfresuz  46518  funressnfv  47800  dfdfat2  47885  resinsn  49670  resinsnALT  49671  tposres0  49675  setrec2lem2  50492