Theorem relres 5461

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 5155	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 3867	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3668	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5160	. 2 ⊢ Rel (𝐵 × V)
5		relss 5240	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3231   ∩ cin 3606   ⊆ wss 3607   × cxp 5141   ↾ cres 5145  Rel wrel 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-opab 4746  df-xp 5149  df-rel 5150  df-res 5155

This theorem is referenced by:  elres  5470  iss  5482  dfres2  5488  restidsing  5493  restidsingOLD  5494  issref  5544  asymref  5547  poirr2  5555  cnvcnvres  5633  resco  5677  coeq0  5682  ressn  5709  funssres  5968  fnresdisj  6039  fnres  6045  fresaunres2  6114  fcnvres  6120  nfunsn  6263  dffv2  6310  fsnunfv  6494  resiexg  7144  resfunexgALT  7171  domss2  8160  fidomdm  8284  dmct  9384  relexp0rel  13821  setsres  15948  pospo  17020  metustid  22406  ovoliunlem1  23316  dvres  23720  dvres2  23721  dvlog  24442  efopnlem2  24448  h2hlm  27965  hlimcaui  28221  funresdm1  29542  dfpo2  31771  eqfunresadj  31785  dfrdg2  31825  funpartfun  32175  brres2  34176  elecres  34183  br1cnvssrres  34395  mapfzcons1  37597  diophrw  37639  eldioph2lem1  37640  eldioph2lem2  37641  undmrnresiss  38227  rtrclexi  38245  brfvrcld2  38301  relexpiidm  38313  rp-imass  38382  idhe  38398  limsupresuz  40253  liminfresuz  40334  funressnfv  41529  dfdfat2  41532  setrec2lem2  42766