Theorem relres 5965

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 5643	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4197	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3990	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5649	. 2 ⊢ Rel (𝐵 × V)
5		relss 5736	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3444   ∩ cin 3910   ⊆ wss 3911   × cxp 5629   ↾ cres 5633  Rel wrel 5636

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-opab 5165  df-xp 5637  df-rel 5638  df-res 5643

This theorem is referenced by:  relresdm1  5993  iss  5995  dfres2  6001  restidsing  6013  asymref  6077  poirr2  6085  cnvcnvres  6166  resco  6211  coeq0  6216  resssxp  6231  ressn  6246  dfpo2  6257  snres0  6259  funssres  6544  fnresdisj  6620  fnres  6627  fresaunres2  6714  fcnvres  6719  nfunsn  6882  dffv2  6938  fsnunfv  7143  eqfunresadj  7317  resfunexgALT  7906  elecres  8696  domss2  9077  fidomdm  9261  ttrclco  9647  cottrcl  9648  dmttrcl  9650  rnttrcl  9651  frmin  9678  frrlem16  9687  frr1  9688  dmct  10453  relexp0rel  14979  setsres  17124  pospo  18284  metustid  24475  ovoliunlem1  25436  dvres  25845  dvres2  25846  dvlog  26593  efopnlem2  26599  noetasuplem2  27679  noetainflem2  27683  h2hlm  30959  hlimcaui  31215  dfrdg2  35776  funpartfun  35924  bj-idreseq  37143  bj-idreseqb  37144  brres2  38250  br1cnvssrres  38489  refrelressn  38508  trrelressn  38567  dfeldisj2  38703  dfeldisj3  38704  dfeldisj4  38705  disjres  38729  antisymrelres  38748  antisymrelressn  38749  mapfzcons1  42698  diophrw  42740  eldioph2lem1  42741  eldioph2lem2  42742  undmrnresiss  43586  brfvrcld2  43674  relexpiidm  43686  limsupresuz  45694  liminfresuz  45775  funressnfv  47037  dfdfat2  47122  resinsn  48853  resinsnALT  48854  tposres0  48858  setrec2lem2  49676