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

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 ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦

Proof

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