Definition df-res 2430

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24.

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 2412	. 2 class (A ↾ B)
4		cvv 1348	. . . 4 class V
5	2, 4	cxp 2408	. . 3 class (B × V)
6	1, 5	cin 1486	. 2 class (A ∩ (B × V))
7	3, 6	wceq 1091	1 wff (A ↾ B) = (A ∩ (B × V))

This definition is referenced by:  reseq1 2575  reseq2 2576  hbres 2577  res0 2578  opelres 2579  resundi 2582  resundir 2583  resss 2587  rescom 2588  ssres 2589  ssres2 2590  relres 2591  resabs1 2592  resabs2 2593  resexg 2597  resopab 2598  dfima2 2604  resdisj 2656

metamath.org