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 φ \to \exists^{} x \in A (ψ \land φ)$

Step	Hyp	Ref	Expression
1		moan	$⊢ \exists^{} x (x \in A \land φ) \to \exists^{} x (ψ \land (x \in A \land φ))$
2		an12	$⊢ (ψ \land (x \in A \land φ)) \leftrightarrow (x \in A \land (ψ \land φ))$
3	2	mobii	$⊢ \exists^{} x (ψ \land (x \in A \land φ)) \leftrightarrow \exists^{} x (x \in A \land (ψ \land φ))$
4	1 3	sylib	$⊢ \exists^{} x (x \in A \land φ) \to \exists^{} x (x \in A \land (ψ \land φ))$
5		df-rmo	$⊢ \exists^{} x \in A φ \leftrightarrow \exists^{} x (x \in A \land φ)$
6		df-rmo	$⊢ \exists^{} x \in A (ψ \land φ) \leftrightarrow \exists^{} x (x \in A \land (ψ \land φ))$
7	4 5 6	3imtr4i	$⊢ \exists^{} x \in A φ \to \exists^{} x \in A (ψ \land φ)$

Metamath Proof Explorer