Theorem relres 5965

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 5637	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4179	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3969	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5643	. 2 ⊢ Rel (𝐵 × V)
5		relss 5732	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3430   ∩ cin 3889   ⊆ wss 3890   × cxp 5623   ↾ cres 5627  Rel wrel 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-opab 5149  df-xp 5631  df-rel 5632  df-res 5637

This theorem is referenced by:  relresdm1  5993  iss  5995  dfres2  6001  restidsing  6013  asymref  6074  poirr2  6082  cnvcnvres  6164  resco  6209  coeq0  6215  resssxp  6229  ressn  6244  dfpo2  6255  snres0  6257  funssres  6537  fnresdisj  6613  fnres  6620  fresaunres2  6707  fcnvres  6712  nfunsn  6874  dffv2  6930  fsnunfv  7136  eqfunresadj  7309  resfunexgALT  7895  elecres  8686  domss2  9068  fidomdm  9238  ttrclco  9633  cottrcl  9634  dmttrcl  9636  rnttrcl  9637  frmin  9667  frrlem16  9676  frr1  9677  dmct  10440  relexp0rel  14993  setsres  17142  pospo  18303  metustid  24532  ovoliunlem1  25482  dvres  25891  dvres2  25892  dvlog  26631  efopnlem2  26637  noetasuplem2  27715  noetainflem2  27719  h2hlm  31069  hlimcaui  31325  dfrdg2  35994  funpartfun  36144  bj-idreseq  37495  bj-idreseqb  37496  brres2  38611  br1cnvssrres  38923  refrelressn  38942  trrelressn  39005  dfeldisj2  39148  dfeldisj3  39149  dfeldisj4  39150  disjres  39182  antisymrelres  39204  antisymrelressn  39205  mapfzcons1  43166  diophrw  43208  eldioph2lem1  43209  eldioph2lem2  43210  undmrnresiss  44052  brfvrcld2  44140  relexpiidm  44152  limsupresuz  46152  liminfresuz  46233  funressnfv  47506  dfdfat2  47591  resinsn  49362  resinsnALT  49363  tposres0  49367  setrec2lem2  50184