Theorem nalset

Description: No set contains all sets. Theorem 41 of Suppes p. 30. (Contributed by NM, 23-Aug-1993) Remove use of ax-12 and ax-13 . (Revised by BJ, 31-May-2019)

	Ref	Expression
Assertion	nalset	⊢ ¬ ∃ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥

Proof

Step	Hyp	Ref	Expression
1		alexn	⊢ ( ∀ 𝑥 ∃ 𝑦 ¬ 𝑦 ∈ 𝑥 ↔ ¬ ∃ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 )
2		ax-sep	⊢ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) )
3		elequ1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝑦 ↔ 𝑦 ∈ 𝑦 ) )
4		elequ1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
5		elequ1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
6		elequ2	⊢ ( 𝑧 = 𝑦 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑦 ) )
7	5 6	bitrd	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝑧 ↔ 𝑦 ∈ 𝑦 ) )
8	7	notbid	⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑧 ∈ 𝑧 ↔ ¬ 𝑦 ∈ 𝑦 ) )
9	4 8	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ↔ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝑦 ) ) )
10	3 9	bibi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ) ↔ ( 𝑦 ∈ 𝑦 ↔ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝑦 ) ) ) )
11	10	spvv	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ) → ( 𝑦 ∈ 𝑦 ↔ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝑦 ) ) )
12		pclem6	⊢ ( ( 𝑦 ∈ 𝑦 ↔ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝑦 ) ) → ¬ 𝑦 ∈ 𝑥 )
13	11 12	syl	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 ↔ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑧 ∈ 𝑧 ) ) → ¬ 𝑦 ∈ 𝑥 )
14	2 13	eximii	⊢ ∃ 𝑦 ¬ 𝑦 ∈ 𝑥
15	1 14	mpgbi	⊢ ¬ ∃ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥