Theorem relres 5972

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 5644	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4192	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3982	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5650	. 2 ⊢ Rel (𝐵 × V)
5		relss 5739	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3442   ∩ cin 3902   ⊆ wss 3903   × cxp 5630   ↾ cres 5634  Rel wrel 5637

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 3402  df-v 3444  df-in 3910  df-ss 3920  df-opab 5163  df-xp 5638  df-rel 5639  df-res 5644

This theorem is referenced by:  relresdm1  6000  iss  6002  dfres2  6008  restidsing  6020  asymref  6081  poirr2  6089  cnvcnvres  6171  resco  6216  coeq0  6222  resssxp  6236  ressn  6251  dfpo2  6262  snres0  6264  funssres  6544  fnresdisj  6620  fnres  6627  fresaunres2  6714  fcnvres  6719  nfunsn  6881  dffv2  6937  fsnunfv  7143  eqfunresadj  7316  resfunexgALT  7902  elecres  8694  domss2  9076  fidomdm  9246  ttrclco  9639  cottrcl  9640  dmttrcl  9642  rnttrcl  9643  frmin  9673  frrlem16  9682  frr1  9683  dmct  10446  relexp0rel  14972  setsres  17117  pospo  18278  metustid  24510  ovoliunlem1  25471  dvres  25880  dvres2  25881  dvlog  26628  efopnlem2  26634  noetasuplem2  27714  noetainflem2  27718  h2hlm  31068  hlimcaui  31324  dfrdg2  36009  funpartfun  36159  bj-idreseq  37417  bj-idreseqb  37418  brres2  38524  br1cnvssrres  38836  refrelressn  38855  trrelressn  38918  dfeldisj2  39061  dfeldisj3  39062  dfeldisj4  39063  disjres  39095  antisymrelres  39117  antisymrelressn  39118  mapfzcons1  43074  diophrw  43116  eldioph2lem1  43117  eldioph2lem2  43118  undmrnresiss  43960  brfvrcld2  44048  relexpiidm  44060  limsupresuz  46061  liminfresuz  46142  funressnfv  47403  dfdfat2  47488  resinsn  49231  resinsnALT  49232  tposres0  49236  setrec2lem2  50053