Theorem relres 5970

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 4178	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3968	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5649	. 2 ⊢ Rel (𝐵 × V)
5		relss 5738	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3429   ∩ cin 3888   ⊆ wss 3889   × 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906  df-opab 5148  df-xp 5637  df-rel 5638  df-res 5643

This theorem is referenced by:  relresdm1  5998  iss  6000  dfres2  6006  restidsing  6018  asymref  6079  poirr2  6087  cnvcnvres  6169  resco  6214  coeq0  6220  resssxp  6234  ressn  6249  dfpo2  6260  snres0  6262  funssres  6542  fnresdisj  6618  fnres  6625  fresaunres2  6712  fcnvres  6717  nfunsn  6879  dffv2  6935  fsnunfv  7142  eqfunresadj  7315  resfunexgALT  7901  elecres  8692  domss2  9074  fidomdm  9244  ttrclco  9639  cottrcl  9640  dmttrcl  9642  rnttrcl  9643  frmin  9673  frrlem16  9682  frr1  9683  dmct  10446  relexp0rel  14999  setsres  17148  pospo  18309  metustid  24519  ovoliunlem1  25469  dvres  25878  dvres2  25879  dvlog  26615  efopnlem2  26621  noetasuplem2  27698  noetainflem2  27702  h2hlm  31051  hlimcaui  31307  dfrdg2  35975  funpartfun  36125  bj-idreseq  37476  bj-idreseqb  37477  brres2  38594  br1cnvssrres  38906  refrelressn  38925  trrelressn  38988  dfeldisj2  39131  dfeldisj3  39132  dfeldisj4  39133  disjres  39165  antisymrelres  39187  antisymrelressn  39188  mapfzcons1  43149  diophrw  43191  eldioph2lem1  43192  eldioph2lem2  43193  undmrnresiss  44031  brfvrcld2  44119  relexpiidm  44131  limsupresuz  46131  liminfresuz  46212  funressnfv  47491  dfdfat2  47576  resinsn  49347  resinsnALT  49348  tposres0  49352  setrec2lem2  50169