| Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: Extend class notation to include the proper substitution of a class for a set into another class. |
| Ref | Expression |
|---|---|
| vx | set x |
| cA | class A |
| cB | class B |
| Ref | Expression |
|---|---|
| csb | class [A / x]B |
| Colors of variables: wff set class |