Definition df-res 4656

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 4646	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2752	. . . 4 class V
5	2, 4	cxp 4642	. . 3 class (𝐵 × V)
6	1, 5	cin 3143	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1364	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4919  reseq2  4920  nfres  4927  csbresg  4928  res0  4929  opelres  4930  resres  4937  resundi  4938  resundir  4939  resindi  4940  resindir  4941  inres  4942  resdifcom  4943  resiun1  4944  resiun2  4945  resss  4949  ssres  4951  ssres2  4952  relres  4953  xpssres  4960  resopab  4969  ssrnres  5089  imainrect  5092  xpima1  5093  xpima2m  5094  cnvcnv2  5100  resdmres  5138  nfvres  5568  ressnop0  5718