Definition df-res 4272

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 4262	. 2 class (A ↾ B)
4		cvv 2526	. . . 4 class V
5	2, 4	cxp 4258	. . 3 class (B × V)
6	1, 5	cin 2884	. 2 class (A ∩ (B × V))
7	3, 6	wceq 1223	1 wff (A ↾ B) = (A ∩ (B × V))

This definition is referenced by:  reseq1  4521  reseq2  4522  nfres  4529  csbresg  4530  res0  4531  opelres  4532  resres  4539  resundi  4540  resundir  4541  resindi  4542  resindir  4543  inres  4544  resiun1  4545  resiun2  4546  resss  4550  ssres  4552  ssres2  4553  relres  4554  xpssres  4560  resopab  4567  ssrnres  4678  imainrect  4681  xpima1  4682  xpima2m  4683  cnvcnv2  4689  resdmres  4727  nfvres  5119  ressnop0  5257