Definition df-res 4788

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 ∩ (B × 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 4774	. 2 class (A ↾ B)
4		cvv 2859	. . . 4 class V
5	2, 4	cxp 4770	. . 3 class (B × V)
6	1, 5	cin 3208	. 2 class (A ∩ (B × V))
7	3, 6	wceq 1642	1 wff (A ↾ B) = (A ∩ (B × V))

This definition is referenced by:  reseq1  4928  reseq2  4929  nfres  4936  brres  4949  csbresg  4976  res0  4977  resres  4980  resundi  4981  resundir  4982  resindi  4983  resindir  4984  inres  4985  resss  4988  ssres  4990  ssres2  4991  resopab  4999  ssrnres  5059  resdmres  5078  resexg  5116  ressnop0  5436  fvfullfunlem3  5863