Theorem reueq

Description: Equality has existential uniqueness. (Contributed by Mario Carneiro, 1-Sep-2015)

	Ref	Expression
Assertion	reueq	⊢ ( 𝐵 ∈ 𝐴 ↔ ∃! 𝑥 ∈ 𝐴 𝑥 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		risset	⊢ ( 𝐵 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = 𝐵 )
2		moeq	⊢ ∃* 𝑥 𝑥 = 𝐵
3		mormo	⊢ ( ∃* 𝑥 𝑥 = 𝐵 → ∃* 𝑥 ∈ 𝐴 𝑥 = 𝐵 )
4	2 3	ax-mp	⊢ ∃* 𝑥 ∈ 𝐴 𝑥 = 𝐵
5		reu5	⊢ ( ∃! 𝑥 ∈ 𝐴 𝑥 = 𝐵 ↔ ( ∃ 𝑥 ∈ 𝐴 𝑥 = 𝐵 ∧ ∃* 𝑥 ∈ 𝐴 𝑥 = 𝐵 ) )
6	4 5	mpbiran2	⊢ ( ∃! 𝑥 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = 𝐵 )
7	1 6	bitr4i	⊢ ( 𝐵 ∈ 𝐴 ↔ ∃! 𝑥 ∈ 𝐴 𝑥 = 𝐵 )