Theorem relres 5882

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

Syntax hints:  Vcvv 3494   ∩ cin 3935   ⊆ wss 3936   × cxp 5553   ↾ cres 5557  Rel wrel 5560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952  df-opab 5129  df-xp 5561  df-rel 5562  df-res 5567

This theorem is referenced by:  iss  5903  dfres2  5909  restidsing  5922  asymref  5976  poirr2  5984  cnvcnvres  6062  resco  6103  coeq0  6108  ressn  6136  funssres  6398  fnresdisj  6467  fnres  6474  fresaunres2  6550  fcnvres  6556  nfunsn  6707  dffv2  6756  fsnunfv  6949  resfunexgALT  7649  domss2  8676  fidomdm  8801  dmct  9946  relexp0rel  14396  setsres  16525  pospo  17583  metustid  23164  ovoliunlem1  24103  dvres  24509  dvres2  24510  dvlog  25234  efopnlem2  25240  h2hlm  28757  hlimcaui  29013  funresdm1  30355  dfpo2  32991  eqfunresadj  33004  dfrdg2  33040  funpartfun  33404  bj-idreseq  34457  bj-idreseqb  34458  brres2  35544  elecres  35549  br1cnvssrres  35760  dfeldisj2  35966  dfeldisj3  35967  dfeldisj4  35968  mapfzcons1  39334  diophrw  39376  eldioph2lem1  39377  eldioph2lem2  39378  undmrnresiss  39984  brfvrcld2  40057  relexpiidm  40069  rp-imass  40137  limsupresuz  42004  liminfresuz  42085  funressnfv  43298  dfdfat2  43347  setrec2lem2  44817