Theorem relres 5847

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 5531	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4156	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3949	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5537	. 2 ⊢ Rel (𝐵 × V)
5		relss 5620	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3441   ∩ cin 3880   ⊆ wss 3881   × cxp 5517   ↾ cres 5521  Rel wrel 5524

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-opab 5093  df-xp 5525  df-rel 5526  df-res 5531

This theorem is referenced by:  iss  5870  dfres2  5876  restidsing  5889  asymref  5943  poirr2  5951  cnvcnvres  6029  resco  6070  coeq0  6075  resssxp  6089  ressn  6104  funssres  6368  fnresdisj  6439  fnres  6446  fresaunres2  6524  fcnvres  6530  nfunsn  6682  dffv2  6733  fsnunfv  6926  resfunexgALT  7631  domss2  8660  fidomdm  8785  dmct  9935  relexp0rel  14388  setsres  16517  pospo  17575  metustid  23161  ovoliunlem1  24106  dvres  24514  dvres2  24515  dvlog  25242  efopnlem2  25248  h2hlm  28763  hlimcaui  29019  funresdm1  30368  dfpo2  33104  eqfunresadj  33117  dfrdg2  33153  funpartfun  33517  bj-idreseq  34577  bj-idreseqb  34578  brres2  35689  elecres  35694  br1cnvssrres  35905  dfeldisj2  36111  dfeldisj3  36112  dfeldisj4  36113  mapfzcons1  39658  diophrw  39700  eldioph2lem1  39701  eldioph2lem2  39702  undmrnresiss  40304  brfvrcld2  40393  relexpiidm  40405  limsupresuz  42345  liminfresuz  42426  funressnfv  43635  dfdfat2  43684  setrec2lem2  45224