Description: Version of eu6 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 12-Aug-1993) (Proof shortened by Wolf Lammen, 30-Oct-2018) Avoid ax-13 . (Revised by Wolf Lammen, 16-Oct-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | euf.1 | ⊢ Ⅎ 𝑦 𝜑 | |
| Assertion | euf | ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | euf.1 | ⊢ Ⅎ 𝑦 𝜑 | |
| 2 | eu6 | ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) | |
| 3 | nfv | ⊢ Ⅎ 𝑦 𝑥 = 𝑧 | |
| 4 | 1 3 | nfbi | ⊢ Ⅎ 𝑦 ( 𝜑 ↔ 𝑥 = 𝑧 ) |
| 5 | 4 | nfal | ⊢ Ⅎ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) |
| 6 | nfv | ⊢ Ⅎ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) | |
| 7 | equequ2 | ⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑦 ) ) | |
| 8 | 7 | bibi2d | ⊢ ( 𝑧 = 𝑦 → ( ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) |
| 9 | 8 | albidv | ⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) |
| 10 | 5 6 9 | cbvexv1 | ⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) |
| 11 | 2 10 | bitri | ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) |