Description: Bidirectional closure of restricted iota when domain is not empty. (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 24-Dec-2016) (Revised by NM, 13-Sep-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | riotaclb | ⊢ ( ¬ ∅ ∈ 𝐴 → ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | riotacl | ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ) | |
| 2 | riotaund | ⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ∅ ) | |
| 3 | 2 | eleq1d | ⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ↔ ∅ ∈ 𝐴 ) ) |
| 4 | 3 | notbid | ⊢ ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ( ¬ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ↔ ¬ ∅ ∈ 𝐴 ) ) |
| 5 | 4 | biimprcd | ⊢ ( ¬ ∅ ∈ 𝐴 → ( ¬ ∃! 𝑥 ∈ 𝐴 𝜑 → ¬ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ) ) |
| 6 | 5 | con4d | ⊢ ( ¬ ∅ ∈ 𝐴 → ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 → ∃! 𝑥 ∈ 𝐴 𝜑 ) ) |
| 7 | 1 6 | impbid2 | ⊢ ( ¬ ∅ ∈ 𝐴 → ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 ) ) |