Description: Obsolete version of csb0 as of 28-Jun-2024. (Contributed by NM, 18-Aug-2018) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | csb0OLD | |- [_ A / x ]_ (/) = (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | csbconstg | |- ( A e. _V -> [_ A / x ]_ (/) = (/) ) |
|
| 2 | csbprc | |- ( -. A e. _V -> [_ A / x ]_ (/) = (/) ) |
|
| 3 | 1 2 | pm2.61i | |- [_ A / x ]_ (/) = (/) |