Theorem rmoan

Description: Restricted "at most one" still holds when a conjunct is added. (Contributed by NM, 16-Jun-2017)

	Ref	Expression
Assertion	rmoan	$$⊢{\exists }^{*}x\in A\phi \to {\exists }^{*}x\in A\left(\psi \wedge \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		moan	$$⊢{\exists }^{*}x\left(x\in A\wedge \phi \right)\to {\exists }^{*}x\left(\psi \wedge \left(x\in A\wedge \phi \right)\right)$$
2		an12	$$⊢\left(\psi \wedge \left(x\in A\wedge \phi \right)\right)\leftrightarrow \left(x\in A\wedge \left(\psi \wedge \phi \right)\right)$$
3	2	mobii	$$⊢{\exists }^{*}x\left(\psi \wedge \left(x\in A\wedge \phi \right)\right)\leftrightarrow {\exists }^{*}x\left(x\in A\wedge \left(\psi \wedge \phi \right)\right)$$
4	1 3	sylib	$$⊢{\exists }^{*}x\left(x\in A\wedge \phi \right)\to {\exists }^{*}x\left(x\in A\wedge \left(\psi \wedge \phi \right)\right)$$
5		df-rmo	$$⊢{\exists }^{*}x\in A\phi \leftrightarrow {\exists }^{*}x\left(x\in A\wedge \phi \right)$$
6		df-rmo	$$⊢{\exists }^{*}x\in A\left(\psi \wedge \phi \right)\leftrightarrow {\exists }^{*}x\left(x\in A\wedge \left(\psi \wedge \phi \right)\right)$$
7	4 5 6	3imtr4i	$$⊢{\exists }^{*}x\in A\phi \to {\exists }^{*}x\in A\left(\psi \wedge \phi \right)$$