Definition df-res 4357

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example ( F = { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ } ∧ B = { 1 , 2 } ) -> ( F ↾ B ) = { ⟨ 2 , 6 ⟩ } . (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 4347	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2557	. . . 4 class V
5	2, 4	cxp 4343	. . 3 class (𝐵 × V)
6	1, 5	cin 2916	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1243	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4606  reseq2  4607  nfres  4614  csbresg  4615  res0  4616  opelres  4617  resres  4624  resundi  4625  resundir  4626  resindi  4627  resindir  4628  inres  4629  resiun1  4630  resiun2  4631  resss  4635  ssres  4637  ssres2  4638  relres  4639  xpssres  4645  resopab  4652  ssrnres  4763  imainrect  4766  xpima1  4767  xpima2m  4768  cnvcnv2  4774  resdmres  4812  nfvres  5206  ressnop0  5344