Definition df-res 5531

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 15465) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 15413 defines the exponential function, which normally allows the exponent to be a complex number). Another example is that (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 ↾ 𝐵) = {⟨2, 6⟩} (ex-res 28226). We do not introduce a special syntax for the corestriction of a class: it will be expressed either as the intersection (𝐴 ∩ (V × 𝐵)) or as the converse of the restricted converse (see cnvrescnv 6019). (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 5521	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3441	. . . 4 class V
5	2, 4	cxp 5517	. . 3 class (𝐵 × V)
6	1, 5	cin 3880	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1538	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5536  reseq1  5812  reseq2  5813  nfres  5820  csbres  5821  res0  5822  dfres3  5823  opelres  5824  resres  5831  resundi  5832  resundir  5833  resindi  5834  resindir  5835  inres  5836  resdifcom  5837  resiun1  5838  resiun2  5839  resss  5843  ssres  5845  ssres2  5846  relres  5847  xpssres  5855  elres  5857  resopab  5869  elrid  5880  imainrect  6005  xpima  6006  cnvcnv2  6017  cnvrescnv  6019  resdmres  6056  ressnop0  6892  fndifnfp  6915  tpres  6940  marypha1lem  8881  gsum2d  19085  gsumxp  19089  pjdm  20396  hausdiag  22250  isngp2  23203  ovoliunlem1  24106  xpdisjres  30361  difres  30363  imadifxp  30364  0res  30367  mbfmcst  31627  0rrv  31819  elrn3  33111  nosupbnd2lem1  33328  noetalem2  33331  noetalem3  33332  dfon4  33467  bj-opelresdm  34560  bj-idres  34575  bj-elid6  34585  restrreld  40368  csbresgVD  41601