Theorem moi2

Description: Consequence of "at most one." (Contributed by NM, 29-Jun-2008)

	Ref	Expression
Hypothesis	moi2.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	moi2	$$⊢\left(\left(A\in B\wedge {\exists }^{*}x\phi \right)\wedge \left(\phi \wedge \psi \right)\right)\to x=A$$

Proof

Step	Hyp	Ref	Expression
1		moi2.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2	1	mob2	$$⊢\left(A\in B\wedge {\exists }^{*}x\phi \wedge \phi \right)\to \left(x=A\leftrightarrow \psi \right)$$
3	2	3expa	$$⊢\left(\left(A\in B\wedge {\exists }^{*}x\phi \right)\wedge \phi \right)\to \left(x=A\leftrightarrow \psi \right)$$
4	3	biimprd	$$⊢\left(\left(A\in B\wedge {\exists }^{*}x\phi \right)\wedge \phi \right)\to \left(\psi \to x=A\right)$$
5	4	impr	$$⊢\left(\left(A\in B\wedge {\exists }^{*}x\phi \right)\wedge \left(\phi \wedge \psi \right)\right)\to x=A$$