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 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 ( ∃! 𝑥 𝜑 { 𝑥𝜑 } = ( ℩ 𝑥 𝜑 ) )