Definition df-res 4639

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 4629	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2738	. . . 4 class V
5	2, 4	cxp 4625	. . 3 class (𝐵 × V)
6	1, 5	cin 3129	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1353	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4902  reseq2  4903  nfres  4910  csbresg  4911  res0  4912  opelres  4913  resres  4920  resundi  4921  resundir  4922  resindi  4923  resindir  4924  inres  4925  resdifcom  4926  resiun1  4927  resiun2  4928  resss  4932  ssres  4934  ssres2  4935  relres  4936  xpssres  4943  resopab  4952  ssrnres  5072  imainrect  5075  xpima1  5076  xpima2m  5077  cnvcnv2  5083  resdmres  5121  nfvres  5549  ressnop0  5698