Definition df-res 4705

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 4695	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2776	. . . 4 class V
5	2, 4	cxp 4691	. . 3 class (𝐵 × V)
6	1, 5	cin 3173	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1373	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4972  reseq2  4973  nfres  4980  csbresg  4981  res0  4982  opelres  4983  resres  4990  resundi  4991  resundir  4992  resindi  4993  resindir  4994  inres  4995  resdifcom  4996  resiun1  4997  resiun2  4998  resss  5002  ssres  5004  ssres2  5005  relres  5006  xpssres  5013  resopab  5022  ssrnres  5144  imainrect  5147  xpima1  5148  xpima2m  5149  cnvcnv2  5155  resdmres  5193  nfvres  5633  ressnop0  5788