NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-res GIF version

Definition df-res 4788
Description: Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. (Contributed by SF, 5-Jan-2015.)
Assertion
Ref Expression
df-res (A B) = (A ∩ (B × V))

Detailed syntax breakdown of Definition df-res
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cres 4774 . 2 class (A B)
4 cvv 2859 . . . 4 class V
52, 4cxp 4770 . . 3 class (B × V)
61, 5cin 3208 . 2 class (A ∩ (B × V))
73, 6wceq 1642 1 wff (A B) = (A ∩ (B × V))
Colors of variables: wff setvar class
This definition is referenced by:  reseq1  4928  reseq2  4929  nfres  4936  brres  4949  csbresg  4976  res0  4977  resres  4980  resundi  4981  resundir  4982  resindi  4983  resindir  4984  inres  4985  resss  4988  ssres  4990  ssres2  4991  resopab  4999  ssrnres  5059  resdmres  5078  resexg  5116  ressnop0  5436  fvfullfunlem3  5863
  Copyright terms: Public domain W3C validator