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 | x e/ x } e/ _V

Proof

Step	Hyp	Ref	Expression
1		pm5.19	|- -. ( { x | x e/ x } e. { x | x e/ x } <-> -. { x | x e/ x } e. { x | x e/ x } )
2		sbcnel12g	|- ( { x | x e/ x } e. _V -> ( [. { x | x e/ x } / x ]. x e/ x <-> [_ { x | x e/ x } / x ]_ x e/ [_ { x | x e/ x } / x ]_ x ) )
3		sbc8g	|- ( { x | x e/ x } e. _V -> ( [. { x | x e/ x } / x ]. x e/ x <-> { x | x e/ x } e. { x | x e/ x } ) )
4		df-nel	|- ( [_ { x | x e/ x } / x ]_ x e/ [_ { x | x e/ x } / x ]_ x <-> -. [_ { x | x e/ x } / x ]_ x e. [_ { x | x e/ x } / x ]_ x )
5		csbvarg	|- ( { x | x e/ x } e. _V -> [_ { x | x e/ x } / x ]_ x = { x | x e/ x } )
6	5 5	eleq12d	|- ( { x | x e/ x } e. _V -> ( [_ { x | x e/ x } / x ]_ x e. [_ { x | x e/ x } / x ]_ x <-> { x | x e/ x } e. { x | x e/ x } ) )
7	6	notbid	|- ( { x | x e/ x } e. _V -> ( -. [_ { x | x e/ x } / x ]_ x e. [_ { x | x e/ x } / x ]_ x <-> -. { x | x e/ x } e. { x | x e/ x } ) )
8	4 7	syl5bb	|- ( { x | x e/ x } e. _V -> ( [_ { x | x e/ x } / x ]_ x e/ [_ { x | x e/ x } / x ]_ x <-> -. { x | x e/ x } e. { x | x e/ x } ) )
9	2 3 8	3bitr3d	|- ( { x | x e/ x } e. _V -> ( { x | x e/ x } e. { x | x e/ x } <-> -. { x | x e/ x } e. { x | x e/ x } ) )
10	1 9	mto	|- -. { x | x e/ x } e. _V
11		df-nel	|- ( { x | x e/ x } e/ _V <-> -. { x | x e/ x } e. _V )
12	10 11	mpbir	|- { x | x e/ x } e/ _V