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

Definition df-csb 3137
Description: Define the proper substitution of a class for a set into another class. The underlined brackets distinguish it from the substitution into a wff, wsbc 3046, to prevent ambiguity. Theorem sbcel1g 3155 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3164 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
df-csb  [.  ].
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()

Detailed syntax breakdown of Definition df-csb
StepHypRef Expression
1 vx . . 3
2 cA . . 3
3 cB . . 3
41, 2, 3csb 3136 . 2
5 vy . . . . . 6
65cv 1641 . . . . 5
76, 3wcel 1710 . . . 4
87, 1, 2wsbc 3046 . . 3  [.  ].
98, 5cab 2339 . 2  [.  ].
104, 9wceq 1642 1  [.  ].
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3138  csbeq1  3139  cbvcsb  3140  csbid  3143  csbco  3145  csbexg  3146  csbtt  3148  sbcel12g  3151  sbceqg  3152  csbeq2d  3160  csbvarg  3163  nfcsb1d  3166  nfcsbd  3169  csbie2g  3182  csbnestgf  3184  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201
  Copyright terms: Public domain W3C validator