Theorem morex

Description: Derive membership from uniqueness. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	morex.1	$$⊢B\in \mathrm{V}$$
	morex.2	$$⊢x=B\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	morex	$$⊢\left(\exists x\in A\phi \wedge {\exists }^{*}x\phi \right)\to \left(\psi \to B\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		morex.1	$$⊢B\in \mathrm{V}$$
2		morex.2	$$⊢x=B\to \left(\phi \leftrightarrow \psi \right)$$
3		df-rex	$$⊢\exists x\in A\phi \leftrightarrow \exists x\left(x\in A\wedge \phi \right)$$
4		exancom	$$⊢\exists x\left(x\in A\wedge \phi \right)\leftrightarrow \exists x\left(\phi \wedge x\in A\right)$$
5	3 4	bitri	$$⊢\exists x\in A\phi \leftrightarrow \exists x\left(\phi \wedge x\in A\right)$$
6		nfmo1	$$⊢Ⅎx{\exists }^{*}x\phi$$
7		nfe1	$$⊢Ⅎx\exists x\left(\phi \wedge x\in A\right)$$
8	6 7	nfan	$$⊢Ⅎx\left({\exists }^{*}x\phi \wedge \exists x\left(\phi \wedge x\in A\right)\right)$$
9		mopick	$$⊢\left({\exists }^{*}x\phi \wedge \exists x\left(\phi \wedge x\in A\right)\right)\to \left(\phi \to x\in A\right)$$
10	8 9	alrimi	$$⊢\left({\exists }^{*}x\phi \wedge \exists x\left(\phi \wedge x\in A\right)\right)\to \forall x\left(\phi \to x\in A\right)$$
11		eleq1	$$⊢x=B\to \left(x\in A\leftrightarrow B\in A\right)$$
12	2 11	imbi12d	$$⊢x=B\to \left(\left(\phi \to x\in A\right)\leftrightarrow \left(\psi \to B\in A\right)\right)$$
13	1 12	spcv	$$⊢\forall x\left(\phi \to x\in A\right)\to \left(\psi \to B\in A\right)$$
14	10 13	syl	$$⊢\left({\exists }^{*}x\phi \wedge \exists x\left(\phi \wedge x\in A\right)\right)\to \left(\psi \to B\in A\right)$$
15	5 14	sylan2b	$$⊢\left({\exists }^{*}x\phi \wedge \exists x\in A\phi \right)\to \left(\psi \to B\in A\right)$$
16	15	ancoms	$$⊢\left(\exists x\in A\phi \wedge {\exists }^{*}x\phi \right)\to \left(\psi \to B\in A\right)$$