**Description:** Another way to express existential uniqueness of a wff: its class
abstraction is a singleton. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref | Expression | ||
---|---|---|---|

Assertion | euabsn2 | ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | eu6 | ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) | |

2 | absn | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) | |

3 | 2 | exbii | ⊢ ( ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) |

4 | 1 3 | bitr4i | ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ) |