Metamath Proof Explorer


Theorem aiotaexb

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 )

Proof

Step Hyp Ref Expression
1 intexab ( ∃ 𝑦 { 𝑥𝜑 } = { 𝑦 } ↔ { 𝑦 ∣ { 𝑥𝜑 } = { 𝑦 } } ∈ V )
2 euabsn2 ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 { 𝑥𝜑 } = { 𝑦 } )
3 df-aiota ( ℩' 𝑥 𝜑 ) = { 𝑦 ∣ { 𝑥𝜑 } = { 𝑦 } }
4 3 eleq1i ( ( ℩' 𝑥 𝜑 ) ∈ V ↔ { 𝑦 ∣ { 𝑥𝜑 } = { 𝑦 } } ∈ V )
5 1 2 4 3bitr4i ( ∃! 𝑥 𝜑 ↔ ( ℩' 𝑥 𝜑 ) ∈ V )