Theorem relres 5956

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

Syntax hints:  Vcvv 3436   ∩ cin 3902   ⊆ wss 3903   × cxp 5617   ↾ cres 5621  Rel wrel 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-in 3910  df-ss 3920  df-opab 5155  df-xp 5625  df-rel 5626  df-res 5631

This theorem is referenced by:  relresdm1  5984  iss  5986  dfres2  5992  restidsing  6004  asymref  6065  poirr2  6073  cnvcnvres  6154  resco  6199  coeq0  6204  resssxp  6218  ressn  6233  dfpo2  6244  snres0  6246  funssres  6526  fnresdisj  6602  fnres  6609  fresaunres2  6696  fcnvres  6701  nfunsn  6862  dffv2  6918  fsnunfv  7123  eqfunresadj  7297  resfunexgALT  7883  elecres  8673  domss2  9053  fidomdm  9224  ttrclco  9614  cottrcl  9615  dmttrcl  9617  rnttrcl  9618  frmin  9645  frrlem16  9654  frr1  9655  dmct  10418  relexp0rel  14944  setsres  17089  pospo  18249  metustid  24440  ovoliunlem1  25401  dvres  25810  dvres2  25811  dvlog  26558  efopnlem2  26564  noetasuplem2  27644  noetainflem2  27648  h2hlm  30924  hlimcaui  31180  dfrdg2  35773  funpartfun  35921  bj-idreseq  37140  bj-idreseqb  37141  brres2  38247  br1cnvssrres  38486  refrelressn  38505  trrelressn  38564  dfeldisj2  38700  dfeldisj3  38701  dfeldisj4  38702  disjres  38726  antisymrelres  38745  antisymrelressn  38746  mapfzcons1  42694  diophrw  42736  eldioph2lem1  42737  eldioph2lem2  42738  undmrnresiss  43581  brfvrcld2  43669  relexpiidm  43681  limsupresuz  45688  liminfresuz  45769  funressnfv  47031  dfdfat2  47116  resinsn  48860  resinsnALT  48861  tposres0  48865  setrec2lem2  49683