Theorem relres 6035

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 5712	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4259	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 4043	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5718	. 2 ⊢ Rel (𝐵 × V)
5		relss 5805	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3488   ∩ cin 3975   ⊆ wss 3976   × cxp 5698   ↾ cres 5702  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-opab 5229  df-xp 5706  df-rel 5707  df-res 5712

This theorem is referenced by:  relresdm1  6062  iss  6064  dfres2  6070  restidsing  6082  asymref  6148  poirr2  6156  cnvcnvres  6236  resco  6281  coeq0  6286  resssxp  6301  ressn  6316  dfpo2  6327  snres0  6329  funssres  6622  fnresdisj  6700  fnres  6707  fresaunres2  6793  fcnvres  6798  nfunsn  6962  dffv2  7017  fsnunfv  7221  eqfunresadj  7396  resfunexgALT  7988  domss2  9202  fidomdm  9402  ttrclco  9787  cottrcl  9788  dmttrcl  9790  rnttrcl  9791  frmin  9818  frrlem16  9827  frr1  9828  dmct  10593  relexp0rel  15086  setsres  17225  pospo  18415  metustid  24588  ovoliunlem1  25556  dvres  25966  dvres2  25967  dvlog  26711  efopnlem2  26717  noetasuplem2  27797  noetainflem2  27801  h2hlm  31012  hlimcaui  31268  dfrdg2  35759  funpartfun  35907  bj-idreseq  37128  bj-idreseqb  37129  brres2  38224  elecres  38233  br1cnvssrres  38461  refrelressn  38480  trrelressn  38539  dfeldisj2  38674  dfeldisj3  38675  dfeldisj4  38676  disjres  38700  antisymrelres  38719  antisymrelressn  38720  mapfzcons1  42673  diophrw  42715  eldioph2lem1  42716  eldioph2lem2  42717  undmrnresiss  43566  brfvrcld2  43654  relexpiidm  43666  limsupresuz  45624  liminfresuz  45705  funressnfv  46958  dfdfat2  47043  setrec2lem2  48786