Theorem relres 5976

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

Syntax hints:  Vcvv 3447   ∩ cin 3913   ⊆ wss 3914   × cxp 5636   ↾ cres 5640  Rel wrel 5643

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 3406  df-v 3449  df-in 3921  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645  df-res 5650

This theorem is referenced by:  relresdm1  6004  iss  6006  dfres2  6012  restidsing  6024  asymref  6089  poirr2  6097  cnvcnvres  6178  resco  6223  coeq0  6228  resssxp  6243  ressn  6258  dfpo2  6269  snres0  6271  funssres  6560  fnresdisj  6638  fnres  6645  fresaunres2  6732  fcnvres  6737  nfunsn  6900  dffv2  6956  fsnunfv  7161  eqfunresadj  7335  resfunexgALT  7926  elecres  8719  domss2  9100  fidomdm  9285  ttrclco  9671  cottrcl  9672  dmttrcl  9674  rnttrcl  9675  frmin  9702  frrlem16  9711  frr1  9712  dmct  10477  relexp0rel  15003  setsres  17148  pospo  18304  metustid  24442  ovoliunlem1  25403  dvres  25812  dvres2  25813  dvlog  26560  efopnlem2  26566  noetasuplem2  27646  noetainflem2  27650  h2hlm  30909  hlimcaui  31165  dfrdg2  35783  funpartfun  35931  bj-idreseq  37150  bj-idreseqb  37151  brres2  38257  br1cnvssrres  38496  refrelressn  38515  trrelressn  38574  dfeldisj2  38710  dfeldisj3  38711  dfeldisj4  38712  disjres  38736  antisymrelres  38755  antisymrelressn  38756  mapfzcons1  42705  diophrw  42747  eldioph2lem1  42748  eldioph2lem2  42749  undmrnresiss  43593  brfvrcld2  43681  relexpiidm  43693  limsupresuz  45701  liminfresuz  45782  funressnfv  47044  dfdfat2  47129  resinsn  48860  resinsnALT  48861  tposres0  48865  setrec2lem2  49683