Definition df-res 4763

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

This definition is referenced by:  reseq1  5034  reseq2  5035  nfres  5042  csbresg  5043  res0  5044  opelres  5045  resres  5052  resundi  5053  resundir  5054  resindi  5055  resindir  5056  inres  5057  resdifcom  5058  resiun1  5059  resiun2  5060  resss  5064  ssres  5066  ssres2  5067  relres  5068  xpssres  5075  resopab  5084  ssrnres  5207  imainrect  5210  xpima1  5211  xpima2m  5212  cnvcnv2  5218  resdmres  5256  nfvres  5708  ressnop0  5867