Definition df-res 4280

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 4270	. 2 class (A ↾ B)
4		cvv 2531	. . . 4 class V
5	2, 4	cxp 4266	. . 3 class (B × V)
6	1, 5	cin 2889	. 2 class (A ∩ (B × V))
7	3, 6	wceq 1226	1 wff (A ↾ B) = (A ∩ (B × V))

This definition is referenced by:  reseq1  4529  reseq2  4530  nfres  4537  csbresg  4538  res0  4539  opelres  4540  resres  4547  resundi  4548  resundir  4549  resindi  4550  resindir  4551  inres  4552  resiun1  4553  resiun2  4554  resss  4558  ssres  4560  ssres2  4561  relres  4562  xpssres  4568  resopab  4575  ssrnres  4686  imainrect  4689  xpima1  4690  xpima2m  4691  cnvcnv2  4697  resdmres  4735  nfvres  5127  ressnop0  5265