Theorem relres 6006

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

This proof depends on syntax axioms:  Vcvv 3457   ∩ cin 3905   ⊆ wss 3906   × cxp 5661   ↾ cres 5665  Rel wrel 5668

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913  df-ss 3923  df-opab 5176  df-xp 5669  df-rel 5670  df-res 5675

This theorem is used by:  resindm  6031  relresdm1  6037  iss  6039  dfres2  6045  restidsing  6057  asymref  6118  poirr2  6126  cnvcnvres  6208  resco  6253  coeq0  6259  resssxp  6274  ressn  6290  dfpo2  6301  snres0  6303  funssres  6584  fnresdisj  6659  fnres  6666  fresaunres2  6754  fcnvres  6759  nfunsn  6924  dffv2  6980  fsnunfv  7191  eqfunresadj  7369  resfunexgALT  7951  elecres  8749  domss2  9131  fidomdm  9298  ttrclco  9694  cottrcl  9695  dmttrcl  9697  rnttrcl  9698  frmin  9728  frrlem16  9737  frr1  9738  dmct  10523  relexp0rel  15100  setsres  17262  pospo  18423  metustid  24764  ovoliunlem1  25714  dvres  26123  dvres2  26124  dvlog  26869  efopnlem2  26875  noetasuplem2  27951  noetainflem2  27955  h2hlm  31405  hlimcaui  31661  dfrdg2  36324  funpartfun  36474  bj-idreseq  37865  bj-idreseqb  37866  brres2  38982  br1cnvssrres  39294  refrelressn  39313  trrelressn  39376  dfeldisj2  39519  dfeldisj3  39520  dfeldisj4  39521  disjres  39553  antisymrelres  39575  antisymrelressn  39576  mapfzcons1  43508  diophrw  43550  eldioph2lem1  43551  eldioph2lem2  43552  undmrnresiss  44390  brfvrcld2  44478  relexpiidm  44490  limsupresuz  46477  liminfresuz  46558  funressnfv  47840  dfdfat2  47925  resinsn  49709  resinsnALT  49710  tposres0  49714  setrec2lem2  50531