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	⊢ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∉ V

Proof

Step	Hyp	Ref	Expression
1		pm5.19	⊢ ¬ ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ↔ ¬ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ { 𝑥 ∣ 𝑥 ∉ 𝑥 } )
2		sbcnel12g	⊢ ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ V → ( [ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ] 𝑥 ∉ 𝑥 ↔ ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 ∉ ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 ) )
3		sbc8g	⊢ ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ V → ( [ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ] 𝑥 ∉ 𝑥 ↔ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ) )
4		df-nel	⊢ ( ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 ∉ ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 ↔ ¬ ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 ∈ ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 )
5		csbvarg	⊢ ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ V → ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 = { 𝑥 ∣ 𝑥 ∉ 𝑥 } )
6	5 5	eleq12d	⊢ ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ V → ( ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 ∈ ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 ↔ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ) )
7	6	notbid	⊢ ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ V → ( ¬ ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 ∈ ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 ↔ ¬ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ) )
8	4 7	bitrid	⊢ ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ V → ( ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 ∉ ⦋ { 𝑥 ∣ 𝑥 ∉ 𝑥 } / 𝑥 ⦌ 𝑥 ↔ ¬ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ) )
9	2 3 8	3bitr3d	⊢ ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ V → ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ↔ ¬ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ) )
10	1 9	mto	⊢ ¬ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ V
11		df-nel	⊢ ( { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∉ V ↔ ¬ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∈ V )
12	10 11	mpbir	⊢ { 𝑥 ∣ 𝑥 ∉ 𝑥 } ∉ V