Definition df-res 4632

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

This definition is referenced by:  reseq1  4894  reseq2  4895  nfres  4902  csbresg  4903  res0  4904  opelres  4905  resres  4912  resundi  4913  resundir  4914  resindi  4915  resindir  4916  inres  4917  resdifcom  4918  resiun1  4919  resiun2  4920  resss  4924  ssres  4926  ssres2  4927  relres  4928  xpssres  4935  resopab  4944  ssrnres  5063  imainrect  5066  xpima1  5067  xpima2m  5068  cnvcnv2  5074  resdmres  5112  nfvres  5540  ressnop0  5689