Theorem relres 5346

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 5050	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 3796	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3598	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5150	. 2 ⊢ Rel (𝐵 × V)
5		relss 5129	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540   × cxp 5036   ↾ cres 5040  Rel wrel 5043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-opab 4644  df-xp 5044  df-rel 5045  df-res 5050

This theorem is referenced by:  elres  5355  iss  5367  dfres2  5372  restidsing  5377  restidsingOLD  5378  issref  5428  asymref  5431  poirr2  5439  cnvcnvres  5516  resco  5556  coeq0  5561  ressn  5588  funssres  5844  fnresdisj  5915  fnres  5921  fresaunres2  5989  fcnvres  5995  nfunsn  6135  dffv2  6181  fsnunfv  6358  resiexg  6994  resfunexgALT  7022  domss2  8004  fidomdm  8128  relexp0rel  13625  setsres  15729  pospo  16796  metustid  22169  ovoliunlem1  23077  dvres  23481  dvres2  23482  dvlog  24197  efopnlem2  24203  h2hlm  27221  hlimcaui  27477  dmct  28877  dfpo2  30898  dfrdg2  30945  funpartfun  31220  mapfzcons1  36298  diophrw  36340  eldioph2lem1  36341  eldioph2lem2  36342  undmrnresiss  36929  rtrclexi  36947  brfvrcld2  37003  relexpiidm  37015  rp-imass  37085  idhe  37101  funressnfv  39857  dfdfat2  39860  setrec2lem2  42240