Definition df-res 4733

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 4723	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2800	. . . 4 class V
5	2, 4	cxp 4719	. . 3 class (𝐵 × V)
6	1, 5	cin 3197	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1395	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  5003  reseq2  5004  nfres  5011  csbresg  5012  res0  5013  opelres  5014  resres  5021  resundi  5022  resundir  5023  resindi  5024  resindir  5025  inres  5026  resdifcom  5027  resiun1  5028  resiun2  5029  resss  5033  ssres  5035  ssres2  5036  relres  5037  xpssres  5044  resopab  5053  ssrnres  5175  imainrect  5178  xpima1  5179  xpima2m  5180  cnvcnv2  5186  resdmres  5224  nfvres  5669  ressnop0  5828