Theorem relres 5996

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 5663	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4183	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3977	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5669	. 2 ⊢ Rel (𝐵 × V)
5		relss 5758	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

This proof depends on syntax axioms:  Vcvv 3451   ∩ cin 3898   ⊆ wss 3899   × cxp 5649   ↾ cres 5653  Rel wrel 5656

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916  df-opab 5168  df-xp 5657  df-rel 5658  df-res 5663

This theorem is used by:  resindm  6019  relresdm1  6025  iss  6027  dfres2  6033  restidsing  6045  asymref  6110  poirr2  6118  cnvcnvres  6206  resco  6251  coeq0  6257  resssxp  6272  ressn  6288  dfpo2  6299  snres0  6301  funssres  6584  fnresdisj  6659  fnres  6666  fresaunres2  6754  fcnvres  6759  nfunsn  6924  dffv2  6980  fsnunfv  7192  eqfunresadj  7370  resfunexgALT  7960  elecres  8766  domss2  9155  fidomdm  9323  ttrclco  9719  cottrcl  9720  dmttrcl  9722  rnttrcl  9723  frmin  9753  frrlem16  9762  frr1  9763  setrec2lem2  9976  dmct  10602  dmctOLD  10603  relexp0rel  15190  setsres  17356  pospo  18517  metustid  24873  ovoliunlem1  25823  dvres  26231  dvres2  26232  dvlog  26979  efopnlem2  26985  noetasuplem2  28091  noetainflem2  28095  h2hlm  31582  hlimcaui  31838  dfrdg2  36557  funpartfun  36707  bj-idreseq  38083  bj-idreseqb  38084  brres2  39205  br1cnvssrres  39517  refrelressn  39536  trrelressn  39599  dfeldisj2  39742  dfeldisj3  39743  dfeldisj4  39744  disjres  39776  antisymrelres  39798  antisymrelressn  39799  mapfzcons1  43727  diophrw  43769  eldioph2lem1  43770  eldioph2lem2  43771  undmrnresiss  44603  brfvrcld2  44691  relexpiidm  44703  limsupresuz  46712  liminfresuz  46793  funressnfv  48112  dfdfat2  48197  resinsn  49979  resinsnALT  49980  tposres0  49984