Metamath Proof Explorer

Theorem rru

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 Gino Giotto, 30-Aug-2024)

Ref Expression
Assertion rru 
|- -. { x e. A | -. x e. x } e. A

Proof

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