Definition df-res 4511

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example ( F = { ⟨ 2 , 6 ⟩, ⟨ 3 , 9 ⟩ } ∧ B = { 1 , 2 } ) -> ( F ↾ B ) = { ⟨ 2 , 6 ⟩ } . (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
df-res	⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

Detailed syntax breakdown of Definition df-res

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cres 4501	. 2 class (𝐴 ↾ 𝐵)
4		cvv 2657	. . . 4 class V
5	2, 4	cxp 4497	. . 3 class (𝐵 × V)
6	1, 5	cin 3036	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1314	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  reseq1  4771  reseq2  4772  nfres  4779  csbresg  4780  res0  4781  opelres  4782  resres  4789  resundi  4790  resundir  4791  resindi  4792  resindir  4793  inres  4794  resdifcom  4795  resiun1  4796  resiun2  4797  resss  4801  ssres  4803  ssres2  4804  relres  4805  xpssres  4812  resopab  4821  ssrnres  4939  imainrect  4942  xpima1  4943  xpima2m  4944  cnvcnv2  4950  resdmres  4988  nfvres  5408  ressnop0  5555