Metamath Proof Explorer


Theorem rusbcALT

Description: A version of Russell's paradox which is proven using proper substitution. (Contributed by Andrew Salmon, 18-Jun-2011) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion rusbcALT x|xxV

Proof

Step Hyp Ref Expression
1 pm5.19 ¬x|xxx|xx¬x|xxx|xx
2 sbcnel12g x|xxV[˙x|xx/x]˙xxx|xx/xxx|xx/xx
3 sbc8g x|xxV[˙x|xx/x]˙xxx|xxx|xx
4 df-nel x|xx/xxx|xx/xx¬x|xx/xxx|xx/xx
5 csbvarg x|xxVx|xx/xx=x|xx
6 5 5 eleq12d x|xxVx|xx/xxx|xx/xxx|xxx|xx
7 6 notbid x|xxV¬x|xx/xxx|xx/xx¬x|xxx|xx
8 4 7 syl5bb x|xxVx|xx/xxx|xx/xx¬x|xxx|xx
9 2 3 8 3bitr3d x|xxVx|xxx|xx¬x|xxx|xx
10 1 9 mto ¬x|xxV
11 df-nel x|xxV¬x|xxV
12 10 11 mpbir x|xxV