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 )