Description: A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton. (Contributed by NM, 30-May-2006) (Proof shortened by Mario Carneiro, 14-Nov-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | reusn | ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 } ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | euabsn2 | ⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 } ) | |
| 2 | df-reu | ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) | |
| 3 | df-rab | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } | |
| 4 | 3 | eqeq1i | ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 } ↔ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 } ) |
| 5 | 4 | exbii | ⊢ ( ∃ 𝑦 { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 } ↔ ∃ 𝑦 { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } = { 𝑦 } ) |
| 6 | 1 2 5 | 3bitr4i | ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑦 { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 } ) |