Description: The FOL statement used in the standard proof of Russell's paradox ru . (Contributed by NM, 7-Aug-1994) Extract from proof of ru and reduce axiom usage. (Revised by BJ, 12-Oct-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ru0 | |- -. A. x ( x e. y <-> -. x e. x ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm5.19 | |- -. ( y e. y <-> -. y e. y ) |
|
| 2 | elequ1 | |- ( x = y -> ( x e. y <-> y e. y ) ) |
|
| 3 | elequ12 | |- ( ( x = y /\ x = y ) -> ( x e. x <-> y e. y ) ) |
|
| 4 | 3 | anidms | |- ( x = y -> ( x e. x <-> y e. y ) ) |
| 5 | 4 | notbid | |- ( x = y -> ( -. x e. x <-> -. y e. y ) ) |
| 6 | 2 5 | bibi12d | |- ( x = y -> ( ( x e. y <-> -. x e. x ) <-> ( y e. y <-> -. y e. y ) ) ) |
| 7 | 6 | spvv | |- ( A. x ( x e. y <-> -. x e. x ) -> ( y e. y <-> -. y e. y ) ) |
| 8 | 1 7 | mto | |- -. A. x ( x e. y <-> -. x e. x ) |