Theorem iotain

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

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

Proof

Step	Hyp	Ref	Expression
1		eu6	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
2		vex	⊢ 𝑦 ∈ V
3	2	intsn	⊢ ∩ { 𝑦 } = 𝑦
4		abbi1	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑦 } )
5		df-sn	⊢ { 𝑦 } = { 𝑥 ∣ 𝑥 = 𝑦 }
6	4 5	eqtr4di	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑦 } )
7	6	inteqd	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∩ { 𝑥 ∣ 𝜑 } = ∩ { 𝑦 } )
8		iotaval	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )
9	3 7 8	3eqtr4a	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∩ { 𝑥 ∣ 𝜑 } = ( ℩ 𝑥 𝜑 ) )
10	9	exlimiv	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∩ { 𝑥 ∣ 𝜑 } = ( ℩ 𝑥 𝜑 ) )
11	1 10	sylbi	⊢ ( ∃! 𝑥 𝜑 → ∩ { 𝑥 ∣ 𝜑 } = ( ℩ 𝑥 𝜑 ) )