Definition df-res 4743

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 4733	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2803	. . . 4 class V
5	2, 4	cxp 4729	. . 3 class (𝐵 × V)
6	1, 5	cin 3200	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1398	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  5013  reseq2  5014  nfres  5021  csbresg  5022  res0  5023  opelres  5024  resres  5031  resundi  5032  resundir  5033  resindi  5034  resindir  5035  inres  5036  resdifcom  5037  resiun1  5038  resiun2  5039  resss  5043  ssres  5045  ssres2  5046  relres  5047  xpssres  5054  resopab  5063  ssrnres  5186  imainrect  5189  xpima1  5190  xpima2m  5191  cnvcnv2  5197  resdmres  5235  nfvres  5684  ressnop0  5843