Description: Relative version of Russell's paradox ru (which corresponds to the case A = _V ).
Originally a subproof in pwnss . (Contributed by Stefan O'Rear, 22-Feb-2015) Avoid df-nel . (Revised by Steven Nguyen, 23-Nov-2022) Reduce axiom usage. (Revised by GG, 30-Aug-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rru | |- -. { x e. A | -. x e. x } e. A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq12 | |- ( ( y = { x e. A | -. x e. x } /\ y = { x e. A | -. x e. x } ) -> ( y e. y <-> { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
|
| 2 | 1 | anidms | |- ( y = { x e. A | -. x e. x } -> ( y e. y <-> { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
| 3 | 2 | notbid | |- ( y = { x e. A | -. x e. x } -> ( -. y e. y <-> -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
| 4 | eleq12 | |- ( ( x = y /\ x = y ) -> ( x e. x <-> y e. y ) ) |
|
| 5 | 4 | anidms | |- ( x = y -> ( x e. x <-> y e. y ) ) |
| 6 | 5 | notbid | |- ( x = y -> ( -. x e. x <-> -. y e. y ) ) |
| 7 | 6 | cbvrabv | |- { x e. A | -. x e. x } = { y e. A | -. y e. y } |
| 8 | 3 7 | elrab2 | |- ( { x e. A | -. x e. x } e. { x e. A | -. x e. x } <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) |
| 9 | pclem6 | |- ( ( { x e. A | -. x e. x } e. { x e. A | -. x e. x } <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) -> -. { x e. A | -. x e. x } e. A ) |
|
| 10 | 8 9 | ax-mp | |- -. { x e. A | -. x e. x } e. A |