Definition df-res 4675

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

This definition is referenced by:  reseq1  4940  reseq2  4941  nfres  4948  csbresg  4949  res0  4950  opelres  4951  resres  4958  resundi  4959  resundir  4960  resindi  4961  resindir  4962  inres  4963  resdifcom  4964  resiun1  4965  resiun2  4966  resss  4970  ssres  4972  ssres2  4973  relres  4974  xpssres  4981  resopab  4990  ssrnres  5112  imainrect  5115  xpima1  5116  xpima2m  5117  cnvcnv2  5123  resdmres  5161  nfvres  5592  ressnop0  5743