Metamath Proof Explorer

Theorem ax6vsep

Description: Derive ax6v (a weakened version of ax-6 where x and y must be distinct), from Separation ax-sep and Extensionality ax-ext . See ax6 for the derivation of ax-6 from ax6v . (Contributed by NM, 12-Nov-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6vsep ⊢ ¬ ∀ x ¬ x = y

Proof

Step Hyp Ref Expression
1 ax-sep ⊢ ∃ x ∀ z z ∈ x ↔ z ∈ y ∧ z = z → z = z
2 id ⊢ z = z → z = z
3 2 biantru ⊢ z ∈ y ↔ z ∈ y ∧ z = z → z = z
4 3 bibi2i ⊢ z ∈ x ↔ z ∈ y ↔ z ∈ x ↔ z ∈ y ∧ z = z → z = z
5 4 biimpri ⊢ z ∈ x ↔ z ∈ y ∧ z = z → z = z → z ∈ x ↔ z ∈ y
6 5 alimi ⊢ ∀ z z ∈ x ↔ z ∈ y ∧ z = z → z = z → ∀ z z ∈ x ↔ z ∈ y
7 ax-ext ⊢ ∀ z z ∈ x ↔ z ∈ y → x = y
8 6 7 syl ⊢ ∀ z z ∈ x ↔ z ∈ y ∧ z = z → z = z → x = y
9 8 eximi ⊢ ∃ x ∀ z z ∈ x ↔ z ∈ y ∧ z = z → z = z → ∃ x x = y
10 1 9 ax-mp ⊢ ∃ x x = y
11 df-ex ⊢ ∃ x x = y ↔ ¬ ∀ x ¬ x = y
12 10 11 mpbi ⊢ ¬ ∀ x ¬ x = y