Theorem relres 5920

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 5601	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4163	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3955	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5607	. 2 ⊢ Rel (𝐵 × V)
5		relss 5692	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3432   ∩ cin 3886   ⊆ wss 3887   × cxp 5587   ↾ cres 5591  Rel wrel 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595  df-rel 5596  df-res 5601

This theorem is referenced by:  iss  5943  dfres2  5949  restidsing  5962  asymref  6021  poirr2  6029  cnvcnvres  6108  resco  6154  coeq0  6159  resssxp  6173  ressn  6188  dfpo2  6199  funssres  6478  fnresdisj  6552  fnres  6559  fresaunres2  6646  fcnvres  6651  nfunsn  6811  dffv2  6863  fsnunfv  7059  resfunexgALT  7790  domss2  8923  fidomdm  9096  ttrclco  9476  cottrcl  9477  dmttrcl  9479  rnttrcl  9480  frmin  9507  frrlem16  9516  frr1  9517  dmct  10280  relexp0rel  14748  setsres  16879  pospo  18063  metustid  23710  ovoliunlem1  24666  dvres  25075  dvres2  25076  dvlog  25806  efopnlem2  25812  h2hlm  29342  hlimcaui  29598  funresdm1  30944  snres0  33675  eqfunresadj  33735  dfrdg2  33771  noetasuplem2  33937  noetainflem2  33941  funpartfun  34245  bj-idreseq  35333  bj-idreseqb  35334  brres2  36407  elecres  36412  br1cnvssrres  36623  dfeldisj2  36829  dfeldisj3  36830  dfeldisj4  36831  mapfzcons1  40539  diophrw  40581  eldioph2lem1  40582  eldioph2lem2  40583  undmrnresiss  41212  brfvrcld2  41300  relexpiidm  41312  limsupresuz  43244  liminfresuz  43325  funressnfv  44537  dfdfat2  44620  setrec2lem2  46400