Theorem riota1

Description: Property of restricted iota. Compare iota1 . (Contributed by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Assertion	riota1	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
2		iota1	⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) = 𝑥 ) )
3	1 2	sylbi	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) = 𝑥 ) )
4		df-riota	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
5	4	eqeq1i	⊢ ( ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = 𝑥 ↔ ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) = 𝑥 )
6	3 5	bitr4di	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = 𝑥 ) )