Definition df-res 4788

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 ↾ 𝐵) = {⟨2, 6⟩}. We do not introduce a special syntax for the corestriction of a class: it will be expressed either as the intersection (𝐴 ∩ (V × 𝐵)) or as the converse of the restricted converse. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
df-res	⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

Detailed syntax breakdown of Definition df-res

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cres 4778	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2821	. . . 4 class V
5	2, 4	cxp 4774	. . 3 class (𝐵 × V)
6	1, 5	cin 3219	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1402	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is used by:  reseq1  5059  reseq2  5060  nfres  5067  csbresg  5068  res0  5069  opelres  5070  resres  5077  resundi  5078  resundir  5079  resindi  5080  resindir  5081  inres  5082  resdifcom  5083  resiun1  5084  resiun2  5085  resss  5089  ssres  5091  ssres2  5092  relres  5093  xpssres  5100  resopab  5110  ssrnres  5233  imainrect  5236  xpima1  5237  xpima2m  5238  cnvcnv2  5244  resdmres  5282  nfvres  5735  ressnop0  5899