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 ¬xA|¬xxA

Proof

Step Hyp Ref Expression
1 eleq12 y=xA|¬xxy=xA|¬xxyyxA|¬xxxA|¬xx
2 1 anidms y=xA|¬xxyyxA|¬xxxA|¬xx
3 2 notbid y=xA|¬xx¬yy¬xA|¬xxxA|¬xx
4 eleq12 x=yx=yxxyy
5 4 anidms x=yxxyy
6 5 notbid x=y¬xx¬yy
7 6 cbvrabv xA|¬xx=yA|¬yy
8 3 7 elrab2 xA|¬xxxA|¬xxxA|¬xxA¬xA|¬xxxA|¬xx
9 pclem6 xA|¬xxxA|¬xxxA|¬xxA¬xA|¬xxxA|¬xx¬xA|¬xxA
10 8 9 ax-mp ¬xA|¬xxA