Definition df-res 4737

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 4727	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2802	. . . 4 class V
5	2, 4	cxp 4723	. . 3 class (𝐵 × V)
6	1, 5	cin 3199	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1397	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  5007  reseq2  5008  nfres  5015  csbresg  5016  res0  5017  opelres  5018  resres  5025  resundi  5026  resundir  5027  resindi  5028  resindir  5029  inres  5030  resdifcom  5031  resiun1  5032  resiun2  5033  resss  5037  ssres  5039  ssres2  5040  relres  5041  xpssres  5048  resopab  5057  ssrnres  5179  imainrect  5182  xpima1  5183  xpima2m  5184  cnvcnv2  5190  resdmres  5228  nfvres  5675  ressnop0  5834