Theorem relres 6011

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 5689	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4230	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 4017	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5695	. 2 ⊢ Rel (𝐵 × V)
5		relss 5782	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3472   ∩ cin 3948   ⊆ wss 3949   × cxp 5675   ↾ cres 5679  Rel wrel 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683  df-rel 5684  df-res 5689

This theorem is referenced by:  relresdm1  6034  iss  6036  dfres2  6042  restidsing  6053  asymref  6118  poirr2  6126  cnvcnvres  6205  resco  6250  coeq0  6255  resssxp  6270  ressn  6285  dfpo2  6296  snres0  6298  funssres  6593  fnresdisj  6671  fnres  6678  fresaunres2  6764  fcnvres  6769  nfunsn  6934  dffv2  6987  fsnunfv  7188  eqfunresadj  7361  resfunexgALT  7938  domss2  9140  fidomdm  9333  ttrclco  9717  cottrcl  9718  dmttrcl  9720  rnttrcl  9721  frmin  9748  frrlem16  9757  frr1  9758  dmct  10523  relexp0rel  14990  setsres  17117  pospo  18304  metustid  24285  ovoliunlem1  25253  dvres  25662  dvres2  25663  dvlog  26393  efopnlem2  26399  noetasuplem2  27471  noetainflem2  27475  h2hlm  30498  hlimcaui  30754  dfrdg2  35069  funpartfun  35217  bj-idreseq  36348  bj-idreseqb  36349  brres2  37441  elecres  37450  br1cnvssrres  37680  refrelressn  37699  trrelressn  37758  dfeldisj2  37893  dfeldisj3  37894  dfeldisj4  37895  disjres  37919  antisymrelres  37938  antisymrelressn  37939  mapfzcons1  41759  diophrw  41801  eldioph2lem1  41802  eldioph2lem2  41803  undmrnresiss  42659  brfvrcld2  42747  relexpiidm  42759  limsupresuz  44719  liminfresuz  44800  funressnfv  46053  dfdfat2  46136  setrec2lem2  47828