Theorem moeq

Description: There exists at most one set equal to a given class. (Contributed by NM, 8-Mar-1995) Shorten combined proofs of moeq and eueq . (Proof shortened by BJ, 24-Sep-2022)

	Ref	Expression
Assertion	moeq	$$⊢{\exists }^{*}xx=A$$

Proof

Step	Hyp	Ref	Expression
1		eqtr3	$$⊢\left(x=A\wedge y=A\right)\to x=y$$
2	1	gen2	$$⊢\forall x\forall y\left(\left(x=A\wedge y=A\right)\to x=y\right)$$
3		eqeq1	$$⊢x=y\to \left(x=A\leftrightarrow y=A\right)$$
4	3	mo4	$$⊢{\exists }^{*}xx=A\leftrightarrow \forall x\forall y\left(\left(x=A\wedge y=A\right)\to x=y\right)$$
5	2 4	mpbir	$$⊢{\exists }^{*}xx=A$$