MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-csb Unicode version

Definition df-csb 3289
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 3186, to prevent ambiguity. Theorem sbcel1g 3681 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3701 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
df-csb
Distinct variable groups:   ,   ,   ,

Detailed syntax breakdown of Definition df-csb
StepHypRef Expression
1 vx . . 3
2 cA . . 3
3 cB . . 3
41, 2, 3csb 3288 . 2
5 vy . . . . . 6
65cv 1368 . . . . 5
76, 3wcel 1756 . . . 4
87, 1, 2wsbc 3186 . . 3
98, 5cab 2429 . 2
104, 9wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3290  csbeq1  3291  csbeq2  3292  cbvcsb  3293  csbid  3296  csbco  3298  csbtt  3299  nfcsb1d  3302  nfcsbd  3305  csbie2g  3318  cbvralcsf  3319  cbvreucsf  3321  cbvrabcsf  3322  csbprc  3673  sbcel12  3675  sbcel12gOLD  3676  sbceqg  3677  csbeq2d  3686  csbnestgf  3692  csbvarg  3700  csbexg  4424  csbexgOLD  4426  csbcom2fi  28938  csbgfi  28939  bj-csbsnlem  32405  bj-csbprc  32411
  Copyright terms: Public domain W3C validator