Description: The alternate iota over a wff ph is a set iff there is a unique value x satisfying ph . (Contributed by AV, 25-Aug-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | aiotaexb | ⊢ ( ∃! 𝑥 𝜑 ↔ ( ℩' 𝑥 𝜑 ) ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | intexab | ⊢ ( ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ∈ V ) | |
2 | euabsn2 | ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ) | |
3 | df-aiota | ⊢ ( ℩' 𝑥 𝜑 ) = ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } | |
4 | 3 | eleq1i | ⊢ ( ( ℩' 𝑥 𝜑 ) ∈ V ↔ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ∈ V ) |
5 | 1 2 4 | 3bitr4i | ⊢ ( ∃! 𝑥 𝜑 ↔ ( ℩' 𝑥 𝜑 ) ∈ V ) |