Theorem relres 6025

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 5700	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4245	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 4029	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5706	. 2 ⊢ Rel (𝐵 × V)
5		relss 5793	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3477   ∩ cin 3961   ⊆ wss 3962   × cxp 5686   ↾ cres 5690  Rel wrel 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979  df-opab 5210  df-xp 5694  df-rel 5695  df-res 5700

This theorem is referenced by:  relresdm1  6052  iss  6054  dfres2  6060  restidsing  6072  asymref  6138  poirr2  6146  cnvcnvres  6226  resco  6271  coeq0  6276  resssxp  6291  ressn  6306  dfpo2  6317  snres0  6319  funssres  6611  fnresdisj  6688  fnres  6695  fresaunres2  6780  fcnvres  6785  nfunsn  6948  dffv2  7003  fsnunfv  7206  eqfunresadj  7379  resfunexgALT  7970  domss2  9174  fidomdm  9371  ttrclco  9755  cottrcl  9756  dmttrcl  9758  rnttrcl  9759  frmin  9786  frrlem16  9795  frr1  9796  dmct  10561  relexp0rel  15072  setsres  17211  pospo  18402  metustid  24582  ovoliunlem1  25550  dvres  25960  dvres2  25961  dvlog  26707  efopnlem2  26713  noetasuplem2  27793  noetainflem2  27797  h2hlm  31008  hlimcaui  31264  dfrdg2  35776  funpartfun  35924  bj-idreseq  37144  bj-idreseqb  37145  brres2  38249  elecres  38258  br1cnvssrres  38486  refrelressn  38505  trrelressn  38564  dfeldisj2  38699  dfeldisj3  38700  dfeldisj4  38701  disjres  38725  antisymrelres  38744  antisymrelressn  38745  mapfzcons1  42704  diophrw  42746  eldioph2lem1  42747  eldioph2lem2  42748  undmrnresiss  43593  brfvrcld2  43681  relexpiidm  43693  limsupresuz  45658  liminfresuz  45739  funressnfv  46992  dfdfat2  47077  setrec2lem2  48924