Definition df-res 3271

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 3253	. 2 class (A |` B)
4		cvv 1857	. . . 4 class V
5	2, 4	cxp 3249	. . 3 class (B X. V)
6	1, 5	cin 2098	. 2 class (A i^i (B X. V))
7	3, 6	wceq 992	1 wff (A |` B) = (A i^i (B X. V))

This definition is referenced by:  reseq1 3455  reseq2 3456  hbres 3457  res0 3458  opelres 3459  resres 3464  resundi 3465  resundir 3466  resindi 3467  resindir 3468  inres 3469  resss 3473  ssres 3475  ssres2 3476  relres 3477  resexg 3484  resopab 3485  dfima2 3497  resdisj 3556  ssrnres 3566  cnvcnv2 3571  rescnvcnv 3591  resdmres 3595  residcp 10806

Copyright terms: Public domain