Definition df-res 5671

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16212) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16157 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 30907). 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 6193). (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 5661	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3453	. . . 4 class V
5	2, 4	cxp 5657	. . 3 class (𝐵 × V)
6	1, 5	cin 3901	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1570	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is used by:  inxpssres  5676  reseq1  5970  reseq2  5971  nfres  5978  csbres  5979  res0  5980  dfres3  5981  opelres  5982  resres  5989  resundi  5990  resundir  5991  resindi  5992  resindir  5993  inres  5994  resdifcom  5995  resiun1  5996  resiun2  5997  resss  5998  ssres  6000  ssres2  6001  relres  6002  xpssres  6015  elres  6017  resopab  6034  elrid  6046  imainrect  6178  xpima  6179  cnvcnv2  6190  cnvrescnv  6193  resdmres  6232  resdifdi  6236  resdifdir  6237  ressnop0  7153  fndifnfp  7177  tpres  7203  marypha1lem  9406  gsum2d  20100  gsumxp  20104  pjdm  21921  hausdiag  23872  isngp2  24824  ovoliunlem1  25731  nosupbnd2lem1  27949  noetasuplem3  27969  noetasuplem4  27970  xpdisjres  33058  difres  33060  imadifxp  33061  0res  33063  mbfmcst  34757  0rrv  34949  elrn3  36328  dfon4  36457  bj-opelresdm  37884  bj-idres  37899  bj-elid6  37909  br1cnvres  39009  restrreld  44494  csbresgVD  45704