# 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 ${⊢}\left\{{x}|{x}\notin {x}\right\}\notin \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 pm5.19 ${⊢}¬\left(\left\{{x}|{x}\notin {x}\right\}\in \left\{{x}|{x}\notin {x}\right\}↔¬\left\{{x}|{x}\notin {x}\right\}\in \left\{{x}|{x}\notin {x}\right\}\right)$
2 sbcnel12g
3 sbc8g
4 df-nel
5 csbvarg
6 5 5 eleq12d
7 6 notbid
8 4 7 syl5bb
9 2 3 8 3bitr3d ${⊢}\left\{{x}|{x}\notin {x}\right\}\in \mathrm{V}\to \left(\left\{{x}|{x}\notin {x}\right\}\in \left\{{x}|{x}\notin {x}\right\}↔¬\left\{{x}|{x}\notin {x}\right\}\in \left\{{x}|{x}\notin {x}\right\}\right)$
10 1 9 mto ${⊢}¬\left\{{x}|{x}\notin {x}\right\}\in \mathrm{V}$
11 df-nel ${⊢}\left\{{x}|{x}\notin {x}\right\}\notin \mathrm{V}↔¬\left\{{x}|{x}\notin {x}\right\}\in \mathrm{V}$
12 10 11 mpbir ${⊢}\left\{{x}|{x}\notin {x}\right\}\notin \mathrm{V}$