Definition df-res 5673

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16175) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16120 defines the exponential function, which normally allows the exponent to be a complex number). Another example is (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 ↾ 𝐵) = {⟨2, 6⟩} (ex-res 30758). 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 6194). (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 5663	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3453	. . . 4 class V
5	2, 4	cxp 5659	. . 3 class (𝐵 × V)
6	1, 5	cin 3903	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1568	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5678  reseq1  5972  reseq2  5973  nfres  5980  csbres  5981  res0  5982  dfres3  5983  opelres  5984  resres  5991  resundi  5992  resundir  5993  resindi  5994  resindir  5995  inres  5996  resdifcom  5997  resiun1  5998  resiun2  5999  resss  6000  ssres  6002  ssres2  6003  relres  6004  xpssres  6017  elres  6019  resopab  6036  elrid  6048  imainrect  6179  xpima  6180  cnvcnv2  6191  cnvrescnv  6194  resdmres  6233  resdifdi  6237  resdifdir  6238  ressnop0  7150  fndifnfp  7174  tpres  7199  marypha1lem  9392  gsum2d  20041  gsumxp  20045  pjdm  21836  hausdiag  23781  isngp2  24733  ovoliunlem1  25640  nosupbnd2lem1  27855  noetasuplem3  27875  noetasuplem4  27876  xpdisjres  32909  difres  32911  imadifxp  32912  0res  32914  mbfmcst  34615  0rrv  34807  elrn3  36208  dfon4  36337  bj-opelresdm  37733  bj-idres  37748  bj-elid6  37758  br1cnvres  38869  restrreld  44341  csbresgVD  45551