Theorem relres 6005

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 5674	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4198	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3991	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5680	. 2 ⊢ Rel (𝐵 × V)
5		relss 5769	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3463   ∩ cin 3912   ⊆ wss 3913   × cxp 5660   ↾ cres 5664  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-in 3920  df-ss 3930  df-opab 5178  df-xp 5668  df-rel 5669  df-res 5674

This theorem is referenced by:  resindm  6030  relresdm1  6036  iss  6038  dfres2  6044  restidsing  6056  asymref  6117  poirr2  6125  cnvcnvres  6207  resco  6252  coeq0  6258  resssxp  6272  ressn  6287  dfpo2  6298  snres0  6300  funssres  6581  fnresdisj  6656  fnres  6663  fresaunres2  6751  fcnvres  6756  nfunsn  6921  dffv2  6977  fsnunfv  7186  eqfunresadj  7359  resfunexgALT  7945  elecres  8743  domss2  9124  fidomdm  9291  ttrclco  9687  cottrcl  9688  dmttrcl  9690  rnttrcl  9691  frmin  9721  frrlem16  9730  frr1  9731  dmct  10508  relexp0rel  15074  setsres  17238  pospo  18399  metustid  24680  ovoliunlem1  25630  dvres  26039  dvres2  26040  dvlog  26782  efopnlem2  26788  noetasuplem2  27864  noetainflem2  27868  h2hlm  31273  hlimcaui  31529  dfrdg2  36184  funpartfun  36334  bj-idreseq  37694  bj-idreseqb  37695  brres2  38812  br1cnvssrres  39124  refrelressn  39143  trrelressn  39206  dfeldisj2  39349  dfeldisj3  39350  dfeldisj4  39351  disjres  39383  antisymrelres  39405  antisymrelressn  39406  mapfzcons1  43340  diophrw  43382  eldioph2lem1  43383  eldioph2lem2  43384  undmrnresiss  44222  brfvrcld2  44310  relexpiidm  44322  limsupresuz  46309  liminfresuz  46390  funressnfv  47669  dfdfat2  47754  resinsn  49535  resinsnALT  49536  tposres0  49540  setrec2lem2  50357