Theorem relres 5953

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 5626	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4185	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3976	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5632	. 2 ⊢ Rel (𝐵 × V)
5		relss 5721	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3436   ∩ cin 3896   ⊆ wss 3897   × cxp 5612   ↾ cres 5616  Rel wrel 5619

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-opab 5152  df-xp 5620  df-rel 5621  df-res 5626

This theorem is referenced by:  relresdm1  5981  iss  5983  dfres2  5989  restidsing  6001  asymref  6062  poirr2  6070  cnvcnvres  6152  resco  6197  coeq0  6203  resssxp  6217  ressn  6232  dfpo2  6243  snres0  6245  funssres  6525  fnresdisj  6601  fnres  6608  fresaunres2  6695  fcnvres  6700  nfunsn  6861  dffv2  6917  fsnunfv  7121  eqfunresadj  7294  resfunexgALT  7880  elecres  8670  domss2  9049  fidomdm  9218  ttrclco  9608  cottrcl  9609  dmttrcl  9611  rnttrcl  9612  frmin  9642  frrlem16  9651  frr1  9652  dmct  10415  relexp0rel  14944  setsres  17089  pospo  18249  metustid  24469  ovoliunlem1  25430  dvres  25839  dvres2  25840  dvlog  26587  efopnlem2  26593  noetasuplem2  27673  noetainflem2  27677  h2hlm  30960  hlimcaui  31216  dfrdg2  35837  funpartfun  35987  bj-idreseq  37206  bj-idreseqb  37207  brres2  38315  br1cnvssrres  38607  refrelressn  38626  trrelressn  38689  dfeldisj2  38826  dfeldisj3  38827  dfeldisj4  38828  disjres  38852  antisymrelres  38871  antisymrelressn  38872  mapfzcons1  42820  diophrw  42862  eldioph2lem1  42863  eldioph2lem2  42864  undmrnresiss  43707  brfvrcld2  43795  relexpiidm  43807  limsupresuz  45811  liminfresuz  45892  funressnfv  47153  dfdfat2  47238  resinsn  48982  resinsnALT  48983  tposres0  48987  setrec2lem2  49805