Description: Corollary of dtru . This example illustrates the danger of blindly trusting the standard Deduction Theorem without accounting for free variables: the theorem form of this deduction is not valid, as shown by dtrucor2 . (Contributed by NM, 27-Jun-2002)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | dtrucor.1 | |- x = y |
|
| Assertion | dtrucor | |- x =/= y |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dtrucor.1 | |- x = y |
|
| 2 | dtru | |- -. A. x x = y |
|
| 3 | 2 | pm2.21i | |- ( A. x x = y -> x =/= y ) |
| 4 | 3 1 | mpg | |- x =/= y |