Theorem iotauni

Description: Equivalence between two different forms of iota . (Contributed by Andrew Salmon, 12-Jul-2011)

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

Proof

Step	Hyp	Ref	Expression
1		eu6	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) )
2		iotaval	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ( ℩ 𝑥 𝜑 ) = 𝑧 )
3		uniabio	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ∪ { 𝑥 ∣ 𝜑 } = 𝑧 )
4	2 3	eqtr4d	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } )
5	4	exlimiv	⊢ ( ∃ 𝑧 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } )
6	1 5	sylbi	⊢ ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } )