Theorem reueq

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

	Ref	Expression
Assertion	reueq	|- ( B e. A <-> E! x e. A x = B )

Proof

Step	Hyp	Ref	Expression
1		risset	|- ( B e. A <-> E. x e. A x = B )
2		moeq	|- E* x x = B
3		mormo	|- ( E* x x = B -> E* x e. A x = B )
4	2 3	ax-mp	|- E* x e. A x = B
5		reu5	|- ( E! x e. A x = B <-> ( E. x e. A x = B /\ E* x e. A x = B ) )
6	4 5	mpbiran2	|- ( E! x e. A x = B <-> E. x e. A x = B )
7	1 6	bitr4i	|- ( B e. A <-> E! x e. A x = B )