Definition df-res 4300

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	⊢ (A ↾ B) = (A ∩ (B × V))

Detailed syntax breakdown of Definition df-res

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cres 4290	. 2 class (A ↾ B)
4		cvv 2551	. . . 4 class V
5	2, 4	cxp 4286	. . 3 class (B × V)
6	1, 5	cin 2910	. 2 class (A ∩ (B × V))
7	3, 6	wceq 1242	1 wff (A ↾ B) = (A ∩ (B × V))

This definition is referenced by:  reseq1  4549  reseq2  4550  nfres  4557  csbresg  4558  res0  4559  opelres  4560  resres  4567  resundi  4568  resundir  4569  resindi  4570  resindir  4571  inres  4572  resiun1  4573  resiun2  4574  resss  4578  ssres  4580  ssres2  4581  relres  4582  xpssres  4588  resopab  4595  ssrnres  4706  imainrect  4709  xpima1  4710  xpima2m  4711  cnvcnv2  4717  resdmres  4755  nfvres  5149  ressnop0  5287