Definition df-res 4139

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 4121	. 2 class (A |` B)
4		cvv 2538	. . . 4 class _V
5	2, 4	cxp 4117	. . 3 class (B X. _V)
6	1, 5	cin 2826	. 2 class (A i^i (B X. _V))
7	3, 6	wceq 1586	1 wff (A |` B) = (A i^i (B X. _V))

This definition is referenced by:  reseq1 4338  reseq2 4339  hbres 4342  csbresg 4343  res0 4344  opelres 4345  resres 4350  resundi 4351  resundir 4352  resindi 4353  resindir 4354  inres 4355  resss 4359  ssres 4361  ssres2 4362  relres 4363  resopab 4373  ssrnres 4460  cnvcnv2 4466  resdmres 4492  ressnop0 4901  dfsup3OLD 5891  residcp 15102  csbresgVD 17553

Copyright terms: Public domain