Description: Another way to express existential uniqueness of a wff ph : its associated class abstraction { x | ph } is a singleton. Variant of euabsn2 using existential uniqueness for the singleton element instead of existence only. (Contributed by AV, 24-Aug-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | euabsneu | ⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mosneq | ⊢ ∃* 𝑦 { 𝑦 } = { 𝑥 ∣ 𝜑 } | |
| 2 | eqcom | ⊢ ( { 𝑦 } = { 𝑥 ∣ 𝜑 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } ) | |
| 3 | 2 | mobii | ⊢ ( ∃* 𝑦 { 𝑦 } = { 𝑥 ∣ 𝜑 } ↔ ∃* 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ) |
| 4 | 1 3 | mpbi | ⊢ ∃* 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } |
| 5 | 4 | biantru | ⊢ ( ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ( ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ∧ ∃* 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ) ) |
| 6 | euabsn2 | ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ) | |
| 7 | df-eu | ⊢ ( ∃! 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ( ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ∧ ∃* 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ) ) | |
| 8 | 5 6 7 | 3bitr4i | ⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ) |