Definition df-res 4731

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 4721	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2799	. . . 4 class V
5	2, 4	cxp 4717	. . 3 class (𝐵 × V)
6	1, 5	cin 3196	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1395	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4999  reseq2  5000  nfres  5007  csbresg  5008  res0  5009  opelres  5010  resres  5017  resundi  5018  resundir  5019  resindi  5020  resindir  5021  inres  5022  resdifcom  5023  resiun1  5024  resiun2  5025  resss  5029  ssres  5031  ssres2  5032  relres  5033  xpssres  5040  resopab  5049  ssrnres  5171  imainrect  5174  xpima1  5175  xpima2m  5176  cnvcnv2  5182  resdmres  5220  nfvres  5665  ressnop0  5824