Definition df-res 3185

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 3167	. 2 class (A |` B)
4		cvv 1807	. . . 4 class V
5	2, 4	cxp 3163	. . 3 class (B X. V)
6	1, 5	cin 2042	. 2 class (A i^i (B X. V))
7	3, 6	wceq 954	1 wff (A |` B) = (A i^i (B X. V))

This definition is referenced by:  reseq1 3360  reseq2 3361  hbres 3362  res0 3363  opelres 3364  resres 3369  resundi 3370  resundir 3371  resss 3375  ssres 3377  ssres2 3378  relres 3379  resexg 3386  resopab 3387  dfima2 3397  resdisj 3463  ssrnres 3473  cnvcnv2 3479  rescnvcnv 3485  resdmres 3489

Copyright terms: Public domain