Theorem bj-ru0

Description: The FOL part of Russell's paradox ru (see also bj-ru1 , bj-ru ). Use of elequ1 , bj-elequ12 (instead of eleq1 , eleq12d as in ru ) permits to remove dependency on ax-10 , ax-11 , ax-12 , ax-ext , df-sb , df-clab , df-cleq , df-clel . (Contributed by BJ, 12-Oct-2019) (Proof modification is discouraged.)

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

Proof

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