Definition df-res 4708

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 4698	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2779	. . . 4 class V
5	2, 4	cxp 4694	. . 3 class (𝐵 × V)
6	1, 5	cin 3176	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1375	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4975  reseq2  4976  nfres  4983  csbresg  4984  res0  4985  opelres  4986  resres  4993  resundi  4994  resundir  4995  resindi  4996  resindir  4997  inres  4998  resdifcom  4999  resiun1  5000  resiun2  5001  resss  5005  ssres  5007  ssres2  5008  relres  5009  xpssres  5016  resopab  5025  ssrnres  5147  imainrect  5150  xpima1  5151  xpima2m  5152  cnvcnv2  5158  resdmres  5196  nfvres  5637  ressnop0  5793