Definition df-res 4671

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

This definition is referenced by:  reseq1  4936  reseq2  4937  nfres  4944  csbresg  4945  res0  4946  opelres  4947  resres  4954  resundi  4955  resundir  4956  resindi  4957  resindir  4958  inres  4959  resdifcom  4960  resiun1  4961  resiun2  4962  resss  4966  ssres  4968  ssres2  4969  relres  4970  xpssres  4977  resopab  4986  ssrnres  5108  imainrect  5111  xpima1  5112  xpima2m  5113  cnvcnv2  5119  resdmres  5157  nfvres  5588  ressnop0  5739