This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ¬ ∃ x ∀ y y ∈ x

Proof

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