![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ax6vsep | Structured version Visualization version GIF version |
Description: Derive a weakened version of ax-6 1875 ( i.e. ax6v 1876), where 𝑥 and 𝑦 must be distinct, from Separation ax-sep 4709 and Extensionality ax-ext 2590. See ax6 2239 for the derivation of ax-6 1875 from ax6v 1876. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax6vsep | ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-sep 4709 | . . 3 ⊢ ∃𝑥∀𝑧(𝑧 ∈ 𝑥 ↔ (𝑧 ∈ 𝑦 ∧ (𝑧 = 𝑧 → 𝑧 = 𝑧))) | |
2 | id 22 | . . . . . . . . 9 ⊢ (𝑧 = 𝑧 → 𝑧 = 𝑧) | |
3 | 2 | biantru 525 | . . . . . . . 8 ⊢ (𝑧 ∈ 𝑦 ↔ (𝑧 ∈ 𝑦 ∧ (𝑧 = 𝑧 → 𝑧 = 𝑧))) |
4 | 3 | bibi2i 326 | . . . . . . 7 ⊢ ((𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) ↔ (𝑧 ∈ 𝑥 ↔ (𝑧 ∈ 𝑦 ∧ (𝑧 = 𝑧 → 𝑧 = 𝑧)))) |
5 | 4 | biimpri 217 | . . . . . 6 ⊢ ((𝑧 ∈ 𝑥 ↔ (𝑧 ∈ 𝑦 ∧ (𝑧 = 𝑧 → 𝑧 = 𝑧))) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) |
6 | 5 | alimi 1730 | . . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ (𝑧 ∈ 𝑦 ∧ (𝑧 = 𝑧 → 𝑧 = 𝑧))) → ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) |
7 | ax-ext 2590 | . . . . 5 ⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦) | |
8 | 6, 7 | syl 17 | . . . 4 ⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ (𝑧 ∈ 𝑦 ∧ (𝑧 = 𝑧 → 𝑧 = 𝑧))) → 𝑥 = 𝑦) |
9 | 8 | eximi 1752 | . . 3 ⊢ (∃𝑥∀𝑧(𝑧 ∈ 𝑥 ↔ (𝑧 ∈ 𝑦 ∧ (𝑧 = 𝑧 → 𝑧 = 𝑧))) → ∃𝑥 𝑥 = 𝑦) |
10 | 1, 9 | ax-mp 5 | . 2 ⊢ ∃𝑥 𝑥 = 𝑦 |
11 | df-ex 1696 | . 2 ⊢ (∃𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 ¬ 𝑥 = 𝑦) | |
12 | 10, 11 | mpbi 219 | 1 ⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 ∀wal 1473 = wceq 1475 ∃wex 1695 ∈ wcel 1977 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 ax-sep 4709 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |