Definition df-res 4375

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 4365	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2601	. . . 4 class V
5	2, 4	cxp 4361	. . 3 class (𝐵 × V)
6	1, 5	cin 2972	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1284	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4624  reseq2  4625  nfres  4632  csbresg  4633  res0  4634  opelres  4635  resres  4642  resundi  4643  resundir  4644  resindi  4645  resindir  4646  inres  4647  resiun1  4648  resiun2  4649  resss  4653  ssres  4655  ssres2  4656  relres  4657  xpssres  4663  resopab  4672  ssrnres  4783  imainrect  4786  xpima1  4787  xpima2m  4788  cnvcnv2  4794  resdmres  4832  nfvres  5227  ressnop0  5365