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