Metamath Proof Explorer


Theorem iota1

Description: Property of iota. (Contributed by NM, 23-Aug-2011) (Revised by Mario Carneiro, 23-Dec-2016)

Ref Expression
Assertion iota1 ( ∃! 𝑥 𝜑 → ( 𝜑 ↔ ( ℩ 𝑥 𝜑 ) = 𝑥 ) )

Proof

Step Hyp Ref Expression
1 eu6 ( ∃! 𝑥 𝜑 ↔ ∃ 𝑧𝑥 ( 𝜑𝑥 = 𝑧 ) )
2 sp ( ∀ 𝑥 ( 𝜑𝑥 = 𝑧 ) → ( 𝜑𝑥 = 𝑧 ) )
3 iotaval ( ∀ 𝑥 ( 𝜑𝑥 = 𝑧 ) → ( ℩ 𝑥 𝜑 ) = 𝑧 )
4 3 eqeq2d ( ∀ 𝑥 ( 𝜑𝑥 = 𝑧 ) → ( 𝑥 = ( ℩ 𝑥 𝜑 ) ↔ 𝑥 = 𝑧 ) )
5 2 4 bitr4d ( ∀ 𝑥 ( 𝜑𝑥 = 𝑧 ) → ( 𝜑𝑥 = ( ℩ 𝑥 𝜑 ) ) )
6 eqcom ( 𝑥 = ( ℩ 𝑥 𝜑 ) ↔ ( ℩ 𝑥 𝜑 ) = 𝑥 )
7 5 6 bitrdi ( ∀ 𝑥 ( 𝜑𝑥 = 𝑧 ) → ( 𝜑 ↔ ( ℩ 𝑥 𝜑 ) = 𝑥 ) )
8 7 exlimiv ( ∃ 𝑧𝑥 ( 𝜑𝑥 = 𝑧 ) → ( 𝜑 ↔ ( ℩ 𝑥 𝜑 ) = 𝑥 ) )
9 1 8 sylbi ( ∃! 𝑥 𝜑 → ( 𝜑 ↔ ( ℩ 𝑥 𝜑 ) = 𝑥 ) )