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

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 ⊢ ( ∃! 𝑥 𝜑 → ( 𝜑 ↔ ( ℩ 𝑥 𝜑 ) = 𝑥 ) )