Theorem reuabaiotaiota

Description: The iota and the alternate iota over a wff ph are equal iff there is a unique satisfying value of { x | ph } = { y } . (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	reuabaiotaiota	⊢ ( ∃! 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ( ℩ 𝑥 𝜑 ) = ( ℩' 𝑥 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		uniintab	⊢ ( ∃! 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } )
2		df-iota	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } }
3		df-aiota	⊢ ( ℩' 𝑥 𝜑 ) = ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } }
4	2 3	eqeq12i	⊢ ( ( ℩ 𝑥 𝜑 ) = ( ℩' 𝑥 𝜑 ) ↔ ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } )
5	1 4	bitr4i	⊢ ( ∃! 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ( ℩ 𝑥 𝜑 ) = ( ℩' 𝑥 𝜑 ) )