Definition df-res 4616

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 4606	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2726	. . . 4 class V
5	2, 4	cxp 4602	. . 3 class (𝐵 × V)
6	1, 5	cin 3115	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1343	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4878  reseq2  4879  nfres  4886  csbresg  4887  res0  4888  opelres  4889  resres  4896  resundi  4897  resundir  4898  resindi  4899  resindir  4900  inres  4901  resdifcom  4902  resiun1  4903  resiun2  4904  resss  4908  ssres  4910  ssres2  4911  relres  4912  xpssres  4919  resopab  4928  ssrnres  5046  imainrect  5049  xpima1  5050  xpima2m  5051  cnvcnv2  5057  resdmres  5095  nfvres  5519  ressnop0  5666