Description: Two ways to express single-valuedness of a class expression A ( x ) . (Contributed by NM, 14-Oct-2010) (Revised by Mario Carneiro, 18-Nov-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eusv2i | ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfeu1 | ⊢ Ⅎ 𝑦 ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 | |
| 2 | nfcvd | ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 𝑦 ) | |
| 3 | eusvnf | ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 𝐴 ) | |
| 4 | 2 3 | nfeqd | ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → Ⅎ 𝑥 𝑦 = 𝐴 ) |
| 5 | 4 | nfrd | ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → ( ∃ 𝑥 𝑦 = 𝐴 → ∀ 𝑥 𝑦 = 𝐴 ) ) |
| 6 | 19.2 | ⊢ ( ∀ 𝑥 𝑦 = 𝐴 → ∃ 𝑥 𝑦 = 𝐴 ) | |
| 7 | 5 6 | impbid1 | ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → ( ∃ 𝑥 𝑦 = 𝐴 ↔ ∀ 𝑥 𝑦 = 𝐴 ) ) |
| 8 | 1 7 | eubid | ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → ( ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 ↔ ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 ) ) |
| 9 | 8 | ibir | ⊢ ( ∃! 𝑦 ∀ 𝑥 𝑦 = 𝐴 → ∃! 𝑦 ∃ 𝑥 𝑦 = 𝐴 ) |