Definition df-res 4691

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 4681	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2773	. . . 4 class V
5	2, 4	cxp 4677	. . 3 class (𝐵 × V)
6	1, 5	cin 3166	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1373	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4958  reseq2  4959  nfres  4966  csbresg  4967  res0  4968  opelres  4969  resres  4976  resundi  4977  resundir  4978  resindi  4979  resindir  4980  inres  4981  resdifcom  4982  resiun1  4983  resiun2  4984  resss  4988  ssres  4990  ssres2  4991  relres  4992  xpssres  4999  resopab  5008  ssrnres  5130  imainrect  5133  xpima1  5134  xpima2m  5135  cnvcnv2  5141  resdmres  5179  nfvres  5617  ressnop0  5772