Description: No class is a member of itself. Exercise 6 of TakeutiZaring p. 22. (Contributed by NM, 7-Aug-1994) (Proof shortened by Andrew Salmon, 9-Jul-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elirr | |- -. A e. A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( x = A -> x = A ) |
|
| 2 | 1 1 | eleq12d | |- ( x = A -> ( x e. x <-> A e. A ) ) |
| 3 | 2 | notbid | |- ( x = A -> ( -. x e. x <-> -. A e. A ) ) |
| 4 | elirrv | |- -. x e. x |
|
| 5 | 3 4 | vtoclg | |- ( A e. A -> -. A e. A ) |
| 6 | pm2.01 | |- ( ( A e. A -> -. A e. A ) -> -. A e. A ) |
|
| 7 | 5 6 | ax-mp | |- -. A e. A |