Definition df-res 5689

Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16063) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16011 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 29694). 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 6195). (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 5679	. 2 class (𝐴 ↾ 𝐵)
4		cvv 3475	. . . 4 class V
5	2, 4	cxp 5675	. . 3 class (𝐵 × V)
6	1, 5	cin 3948	. 2 class (𝐴 ∩ (𝐵 × V))
7	3, 6	wceq 1542	1 wff (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))

This definition is referenced by:  inxpssres  5694  reseq1  5976  reseq2  5977  nfres  5984  csbres  5985  res0  5986  dfres3  5987  opelres  5988  resres  5995  resundi  5996  resundir  5997  resindi  5998  resindir  5999  inres  6000  resdifcom  6001  resiun1  6002  resiun2  6003  resss  6007  ssres  6009  ssres2  6010  relres  6011  xpssres  6019  elres  6021  resopab  6035  elrid  6046  imainrect  6181  xpima  6182  cnvcnv2  6193  cnvrescnv  6195  resdmres  6232  resdifdi  6236  resdifdir  6237  ressnop0  7151  fndifnfp  7174  tpres  7202  marypha1lem  9428  gsum2d  19840  gsumxp  19844  pjdm  21262  hausdiag  23149  isngp2  24106  ovoliunlem1  25019  nosupbnd2lem1  27218  noetasuplem3  27238  noetasuplem4  27239  xpdisjres  31829  difres  31831  imadifxp  31832  0res  31834  mbfmcst  33258  0rrv  33450  elrn3  34732  dfon4  34865  bj-opelresdm  36026  bj-idres  36041  bj-elid6  36051  br1cnvres  37137  restrreld  42418  csbresgVD  43656