This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 abbi ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑦 } )
5 df-sn ⊢ { 𝑦 } = { 𝑥 ∣ 𝑥 = 𝑦 }
6 4 5 eqtr4di ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑦 } )
7 6 inteqd ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∩ { 𝑥 ∣ 𝜑 } = ∩ { 𝑦 } )
8 iotaval ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )
9 3 7 8 3eqtr4a ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∩ { 𝑥 ∣ 𝜑 } = ( ℩ 𝑥 𝜑 ) )
10 9 exlimiv ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∩ { 𝑥 ∣ 𝜑 } = ( ℩ 𝑥 𝜑 ) )
11 1 10 sylbi ⊢ ( ∃! 𝑥 𝜑 → ∩ { 𝑥 ∣ 𝜑 } = ( ℩ 𝑥 𝜑 ) )