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

Definition df-csb 3435
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 3327, to prevent ambiguity. Theorem sbcel1g 3829 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3849 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 3434 . 2
5 vy . . . . . 6
65cv 1394 . . . . 5
76, 3wcel 1818 . . . 4
87, 1, 2wsbc 3327 . . 3
98, 5cab 2442 . 2
104, 9wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  csb2  3436  csbeq1  3437  csbeq2  3438  cbvcsb  3439  csbid  3442  csbco  3444  csbtt  3445  nfcsb1d  3448  nfcsbd  3451  csbie2g  3465  cbvralcsf  3466  cbvreucsf  3468  cbvrabcsf  3469  csbprc  3821  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  csbeq2d  3834  csbnestgf  3840  csbvarg  3848  csbexg  4584  csbexgOLD  4586  csbcom2fi  30534  csbgfi  30535  bj-csbsnlem  34470  bj-csbprc  34476
  Copyright terms: Public domain W3C validator