Definition df-res 4766

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 4756	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2815	. . . 4 class V
5	2, 4	cxp 4752	. . 3 class (𝐵 × V)
6	1, 5	cin 3213	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1398	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  5037  reseq2  5038  nfres  5045  csbresg  5046  res0  5047  opelres  5048  resres  5055  resundi  5056  resundir  5057  resindi  5058  resindir  5059  inres  5060  resdifcom  5061  resiun1  5062  resiun2  5063  resss  5067  ssres  5069  ssres2  5070  relres  5071  xpssres  5078  resopab  5087  ssrnres  5210  imainrect  5213  xpima1  5214  xpima2m  5215  cnvcnv2  5221  resdmres  5259  nfvres  5711  ressnop0  5870