Description: Soundness justification theorem for eu6 when this was the definition of the unique existential quantifier (note that y and z need not be disjoint, although the weaker theorem with that disjoint variable condition added would be enough to justify the soundness of the definition). See eujustALT for a proof that provides an example of how it can be achieved through the use of dvelim . (Contributed by NM, 11-Mar-2010) (Proof shortened by Andrew Salmon, 9-Jul-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eujust | ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equequ2 | ⊢ ( 𝑦 = 𝑤 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑤 ) ) | |
| 2 | 1 | bibi2d | ⊢ ( 𝑦 = 𝑤 → ( ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( 𝜑 ↔ 𝑥 = 𝑤 ) ) ) |
| 3 | 2 | albidv | ⊢ ( 𝑦 = 𝑤 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) ) ) |
| 4 | 3 | cbvexvw | ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ∃ 𝑤 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) ) |
| 5 | equequ2 | ⊢ ( 𝑤 = 𝑧 → ( 𝑥 = 𝑤 ↔ 𝑥 = 𝑧 ) ) | |
| 6 | 5 | bibi2d | ⊢ ( 𝑤 = 𝑧 → ( ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ( 𝜑 ↔ 𝑥 = 𝑧 ) ) ) |
| 7 | 6 | albidv | ⊢ ( 𝑤 = 𝑧 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) ) |
| 8 | 7 | cbvexvw | ⊢ ( ∃ 𝑤 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑤 ) ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) |
| 9 | 4 8 | bitri | ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) |