Definition df-res 4786

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 4776	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2821	. . . 4 class V
5	2, 4	cxp 4772	. . 3 class (𝐵 × V)
6	1, 5	cin 3219	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1402	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is used by:  reseq1  5057  reseq2  5058  nfres  5065  csbresg  5066  res0  5067  opelres  5068  resres  5075  resundi  5076  resundir  5077  resindi  5078  resindir  5079  inres  5080  resdifcom  5081  resiun1  5082  resiun2  5083  resss  5087  ssres  5089  ssres2  5090  relres  5091  xpssres  5098  resopab  5107  ssrnres  5230  imainrect  5233  xpima1  5234  xpima2m  5235  cnvcnv2  5241  resdmres  5279  nfvres  5732  ressnop0  5896