Definition df-res 4672

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 4662	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2760	. . . 4 class V
5	2, 4	cxp 4658	. . 3 class (𝐵 × V)
6	1, 5	cin 3153	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1364	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4937  reseq2  4938  nfres  4945  csbresg  4946  res0  4947  opelres  4948  resres  4955  resundi  4956  resundir  4957  resindi  4958  resindir  4959  inres  4960  resdifcom  4961  resiun1  4962  resiun2  4963  resss  4967  ssres  4969  ssres2  4970  relres  4971  xpssres  4978  resopab  4987  ssrnres  5109  imainrect  5112  xpima1  5113  xpima2m  5114  cnvcnv2  5120  resdmres  5158  nfvres  5589  ressnop0  5740