Theorem relres 6023

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 5697	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4238	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 4030	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5703	. 2 ⊢ Rel (𝐵 × V)
5		relss 5791	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3480   ∩ cin 3950   ⊆ wss 3951   × cxp 5683   ↾ cres 5687  Rel wrel 5690

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692  df-res 5697

This theorem is referenced by:  relresdm1  6051  iss  6053  dfres2  6059  restidsing  6071  asymref  6136  poirr2  6144  cnvcnvres  6225  resco  6270  coeq0  6275  resssxp  6290  ressn  6305  dfpo2  6316  snres0  6318  funssres  6610  fnresdisj  6688  fnres  6695  fresaunres2  6780  fcnvres  6785  nfunsn  6948  dffv2  7004  fsnunfv  7207  eqfunresadj  7380  resfunexgALT  7972  domss2  9176  fidomdm  9374  ttrclco  9758  cottrcl  9759  dmttrcl  9761  rnttrcl  9762  frmin  9789  frrlem16  9798  frr1  9799  dmct  10564  relexp0rel  15076  setsres  17215  pospo  18390  metustid  24567  ovoliunlem1  25537  dvres  25946  dvres2  25947  dvlog  26693  efopnlem2  26699  noetasuplem2  27779  noetainflem2  27783  h2hlm  30999  hlimcaui  31255  dfrdg2  35796  funpartfun  35944  bj-idreseq  37163  bj-idreseqb  37164  brres2  38269  elecres  38278  br1cnvssrres  38506  refrelressn  38525  trrelressn  38584  dfeldisj2  38719  dfeldisj3  38720  dfeldisj4  38721  disjres  38745  antisymrelres  38764  antisymrelressn  38765  mapfzcons1  42728  diophrw  42770  eldioph2lem1  42771  eldioph2lem2  42772  undmrnresiss  43617  brfvrcld2  43705  relexpiidm  43717  limsupresuz  45718  liminfresuz  45799  funressnfv  47055  dfdfat2  47140  resinsn  48772  resinsnALT  48773  tposres0  48777  setrec2lem2  49213