Definition df-res 4789

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. (Contributed by SF, 5-Jan-2015.)

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 4775	. 2 class (A |` B)
4		cvv 2860	. . . 4 class _V
5	2, 4	cxp 4771	. . 3 class (B X. _V)
6	1, 5	cin 3209	. 2 class (A i^i (B X. _V))
7	3, 6	wceq 1642	1 wff (A |` B) = (A i^i (B X. _V))

This definition is referenced by:  reseq1  4929  reseq2  4930  nfres  4937  brres  4950  csbresg  4977  res0  4978  resres  4981  resundi  4982  resundir  4983  resindi  4984  resindir  4985  inres  4986  resss  4989  ssres  4991  ssres2  4992  resopab  5000  ssrnres  5060  resdmres  5079  resexg  5117  ressnop0  5437  fvfullfunlem3  5864