Definition df-res 3180

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

Assertion

Ref	Expression
df-res	|- (A |` B) = (A i^i (B X. 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 3162	. 2 class (A |` B)
4		cvv 1802	. . . 4 class V
5	2, 4	cxp 3158	. . 3 class (B X. V)
6	1, 5	cin 2036	. 2 class (A i^i (B X. V))
7	3, 6	wceq 953	1 wff (A |` B) = (A i^i (B X. V))

This definition is referenced by:  reseq1 3352  reseq2 3353  hbres 3354  res0 3355  opelres 3356  resres 3361  resundi 3362  resundir 3363  resss 3367  ssres 3369  ssres2 3370  relres 3371  resexg 3378  resopab 3379  dfima2 3389  resdisj 3457  ssrnres 3467  cnvcnv2 3473  rescnvcnv 3479  resdmres 3483

Copyright terms: Public domain