Theorem relres 5909

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 5592	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4160	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3951	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5598	. 2 ⊢ Rel (𝐵 × V)
5		relss 5682	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3422   ∩ cin 3882   ⊆ wss 3883   × cxp 5578   ↾ cres 5582  Rel wrel 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586  df-rel 5587  df-res 5592

This theorem is referenced by:  iss  5932  dfres2  5938  restidsing  5951  asymref  6010  poirr2  6018  cnvcnvres  6097  resco  6143  coeq0  6148  resssxp  6162  ressn  6177  dfpo2  6188  funssres  6462  fnresdisj  6536  fnres  6543  fresaunres2  6630  fcnvres  6635  nfunsn  6793  dffv2  6845  fsnunfv  7041  resfunexgALT  7764  domss2  8872  fidomdm  9026  dmct  10211  relexp0rel  14676  setsres  16807  pospo  17978  metustid  23616  ovoliunlem1  24571  dvres  24980  dvres2  24981  dvlog  25711  efopnlem2  25717  h2hlm  29243  hlimcaui  29499  funresdm1  30845  snres0  33577  eqfunresadj  33641  dfrdg2  33677  ttrclco  33704  cottrcl  33705  dmttrcl  33707  rnttrcl  33708  noetasuplem2  33864  noetainflem2  33868  funpartfun  34172  bj-idreseq  35260  bj-idreseqb  35261  brres2  36334  elecres  36339  br1cnvssrres  36550  dfeldisj2  36756  dfeldisj3  36757  dfeldisj4  36758  mapfzcons1  40455  diophrw  40497  eldioph2lem1  40498  eldioph2lem2  40499  undmrnresiss  41101  brfvrcld2  41189  relexpiidm  41201  limsupresuz  43134  liminfresuz  43215  funressnfv  44424  dfdfat2  44507  setrec2lem2  46286