Theorem reueq

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

	Ref	Expression
Assertion	reueq	$$⊢B\in A\leftrightarrow \exists !x\in Ax=B$$

Proof

Step	Hyp	Ref	Expression
1		risset	$$⊢B\in A\leftrightarrow \exists x\in Ax=B$$
2		moeq	$$⊢{\exists }^{*}xx=B$$
3		mormo	$$⊢{\exists }^{*}xx=B\to {\exists }^{*}x\in Ax=B$$
4	2 3	ax-mp	$$⊢{\exists }^{*}x\in Ax=B$$
5		reu5	$$⊢\exists !x\in Ax=B\leftrightarrow \left(\exists x\in Ax=B\wedge {\exists }^{*}x\in Ax=B\right)$$
6	4 5	mpbiran2	$$⊢\exists !x\in Ax=B\leftrightarrow \exists x\in Ax=B$$
7	1 6	bitr4i	$$⊢B\in A\leftrightarrow \exists !x\in Ax=B$$