Theorem ru0

Description: The FOL statement used in the standard proof of Russell's paradox ru . (Contributed by NM, 7-Aug-1994) Extract from proof of ru and reduce axiom usage. (Revised by BJ, 12-Oct-2019)

	Ref	Expression
Assertion	ru0	⊢ ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		pm5.19	⊢ ¬ ( 𝑦 ∈ 𝑦 ↔ ¬ 𝑦 ∈ 𝑦 )
2		elequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑦 ↔ 𝑦 ∈ 𝑦 ) )
3		elequ12	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) )
4	3	anidms	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) )
5	4	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝑦 ∈ 𝑦 ) )
6	2 5	bibi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑦 ↔ ¬ 𝑦 ∈ 𝑦 ) ) )
7	6	spvv	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥 ) → ( 𝑦 ∈ 𝑦 ↔ ¬ 𝑦 ∈ 𝑦 ) )
8	1 7	mto	⊢ ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ ¬ 𝑥 ∈ 𝑥 )