Definition df-res 4623

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 4613	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2730	. . . 4 class V
5	2, 4	cxp 4609	. . 3 class (𝐵 × V)
6	1, 5	cin 3120	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1348	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4885  reseq2  4886  nfres  4893  csbresg  4894  res0  4895  opelres  4896  resres  4903  resundi  4904  resundir  4905  resindi  4906  resindir  4907  inres  4908  resdifcom  4909  resiun1  4910  resiun2  4911  resss  4915  ssres  4917  ssres2  4918  relres  4919  xpssres  4926  resopab  4935  ssrnres  5053  imainrect  5056  xpima1  5057  xpima2m  5058  cnvcnv2  5064  resdmres  5102  nfvres  5529  ressnop0  5677