Definition df-res 3188

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 3170	. 2 class (A |` B)
4		cvv 1809	. . . 4 class V
5	2, 4	cxp 3166	. . 3 class (B X. V)
6	1, 5	cin 2044	. 2 class (A i^i (B X. V))
7	3, 6	wceq 956	1 wff (A |` B) = (A i^i (B X. V))

This definition is referenced by:  reseq1 3366  reseq2 3367  hbres 3368  res0 3369  opelres 3370  resres 3375  resundi 3376  resundir 3377  resss 3381  ssres 3383  ssres2 3384  relres 3385  resexg 3392  resopab 3393  dfima2 3403  resdisj 3469  ssrnres 3479  cnvcnv2 3485  rescnvcnv 3491  resdmres 3495

Copyright terms: Public domain