Theorem relres 5964

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 5636	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4190	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3980	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5642	. 2 ⊢ Rel (𝐵 × V)
5		relss 5731	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3440   ∩ cin 3900   ⊆ wss 3901   × cxp 5622   ↾ cres 5626  Rel wrel 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908  df-ss 3918  df-opab 5161  df-xp 5630  df-rel 5631  df-res 5636

This theorem is referenced by:  relresdm1  5992  iss  5994  dfres2  6000  restidsing  6012  asymref  6073  poirr2  6081  cnvcnvres  6163  resco  6208  coeq0  6214  resssxp  6228  ressn  6243  dfpo2  6254  snres0  6256  funssres  6536  fnresdisj  6612  fnres  6619  fresaunres2  6706  fcnvres  6711  nfunsn  6873  dffv2  6929  fsnunfv  7133  eqfunresadj  7306  resfunexgALT  7892  elecres  8683  domss2  9064  fidomdm  9234  ttrclco  9627  cottrcl  9628  dmttrcl  9630  rnttrcl  9631  frmin  9661  frrlem16  9670  frr1  9671  dmct  10434  relexp0rel  14960  setsres  17105  pospo  18266  metustid  24498  ovoliunlem1  25459  dvres  25868  dvres2  25869  dvlog  26616  efopnlem2  26622  noetasuplem2  27702  noetainflem2  27706  h2hlm  31055  hlimcaui  31311  dfrdg2  35987  funpartfun  36137  bj-idreseq  37367  bj-idreseqb  37368  brres2  38468  br1cnvssrres  38768  refrelressn  38787  trrelressn  38850  dfeldisj2  38987  dfeldisj3  38988  dfeldisj4  38989  disjres  39013  antisymrelres  39032  antisymrelressn  39033  mapfzcons1  42969  diophrw  43011  eldioph2lem1  43012  eldioph2lem2  43013  undmrnresiss  43855  brfvrcld2  43943  relexpiidm  43955  limsupresuz  45957  liminfresuz  46038  funressnfv  47299  dfdfat2  47384  resinsn  49127  resinsnALT  49128  tposres0  49132  setrec2lem2  49949