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	$$⊢\neg \left(\left\{x|x\notin x\right\}\in \left\{x|x\notin x\right\}\leftrightarrow \neg \left\{x|x\notin x\right\}\in \left\{x|x\notin x\right\}\right)$$
2		sbcnel12g	$$⊢\left\{x|x\notin x\right\}\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left\{x|x\notin x\right\}/x\underset{\dot{}}{]}x\notin x\leftrightarrow ⦋\left\{x|x\notin x\right\}/x⦌x\notin ⦋\left\{x|x\notin x\right\}/x⦌x\right)$$
3		sbc8g	$$⊢\left\{x|x\notin x\right\}\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left\{x|x\notin x\right\}/x\underset{\dot{}}{]}x\notin x\leftrightarrow \left\{x|x\notin x\right\}\in \left\{x|x\notin x\right\}\right)$$
4		df-nel	$$⊢⦋\left\{x|x\notin x\right\}/x⦌x\notin ⦋\left\{x|x\notin x\right\}/x⦌x\leftrightarrow \neg ⦋\left\{x|x\notin x\right\}/x⦌x\in ⦋\left\{x|x\notin x\right\}/x⦌x$$
5		csbvarg	$$⊢\left\{x|x\notin x\right\}\in \mathrm{V}\to ⦋\left\{x|x\notin x\right\}/x⦌x=\left\{x|x\notin x\right\}$$
6	5 5	eleq12d	$$⊢\left\{x|x\notin x\right\}\in \mathrm{V}\to \left(⦋\left\{x|x\notin x\right\}/x⦌x\in ⦋\left\{x|x\notin x\right\}/x⦌x\leftrightarrow \left\{x|x\notin x\right\}\in \left\{x|x\notin x\right\}\right)$$
7	6	notbid	$$⊢\left\{x|x\notin x\right\}\in \mathrm{V}\to \left(\neg ⦋\left\{x|x\notin x\right\}/x⦌x\in ⦋\left\{x|x\notin x\right\}/x⦌x\leftrightarrow \neg \left\{x|x\notin x\right\}\in \left\{x|x\notin x\right\}\right)$$
8	4 7	syl5bb	$$⊢\left\{x|x\notin x\right\}\in \mathrm{V}\to \left(⦋\left\{x|x\notin x\right\}/x⦌x\notin ⦋\left\{x|x\notin x\right\}/x⦌x\leftrightarrow \neg \left\{x|x\notin x\right\}\in \left\{x|x\notin x\right\}\right)$$
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\}\leftrightarrow \neg \left\{x|x\notin x\right\}\in \left\{x|x\notin x\right\}\right)$$
10	1 9	mto	$$⊢\neg \left\{x|x\notin x\right\}\in \mathrm{V}$$
11		df-nel	$$⊢\left\{x|x\notin x\right\}\notin \mathrm{V}\leftrightarrow \neg \left\{x|x\notin x\right\}\in \mathrm{V}$$
12	10 11	mpbir	$$⊢\left\{x|x\notin x\right\}\notin \mathrm{V}$$