Definition df-res 4610

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 4600	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2721	. . . 4 class V
5	2, 4	cxp 4596	. . 3 class (𝐵 × V)
6	1, 5	cin 3110	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1342	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4872  reseq2  4873  nfres  4880  csbresg  4881  res0  4882  opelres  4883  resres  4890  resundi  4891  resundir  4892  resindi  4893  resindir  4894  inres  4895  resdifcom  4896  resiun1  4897  resiun2  4898  resss  4902  ssres  4904  ssres2  4905  relres  4906  xpssres  4913  resopab  4922  ssrnres  5040  imainrect  5043  xpima1  5044  xpima2m  5045  cnvcnv2  5051  resdmres  5089  nfvres  5513  ressnop0  5660