Theorem iotaint

Description: Equivalence between two different forms of iota . (Contributed by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	iotaint	⊢ ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ∩ { 𝑥 ∣ 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		iotauni	⊢ ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } )
2		uniintab	⊢ ( ∃! 𝑥 𝜑 ↔ ∪ { 𝑥 ∣ 𝜑 } = ∩ { 𝑥 ∣ 𝜑 } )
3	2	biimpi	⊢ ( ∃! 𝑥 𝜑 → ∪ { 𝑥 ∣ 𝜑 } = ∩ { 𝑥 ∣ 𝜑 } )
4	1 3	eqtrd	⊢ ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ∩ { 𝑥 ∣ 𝜑 } )