Metamath Proof Explorer

Theorem rmoun

Description: "At most one" restricted existential quantifier for a union implies the same quantifier on both sets. (Contributed by Thierry Arnoux, 27-Nov-2023)

		Ref	Expression
	Assertion	rmoun	$⊢ \exists^{} x \in (A \cup B) φ \to (\exists^{} x \in A φ \land \exists^{*} x \in B φ)$

Proof

Step	Hyp	Ref	Expression
1		mooran2	$⊢ \exists^{} x ((x \in A \land φ) \lor (x \in B \land φ)) \to (\exists^{} x (x \in A \land φ) \land \exists^{*} x (x \in B \land φ))$
2		df-rmo	$⊢ \exists^{} x \in (A \cup B) φ \leftrightarrow \exists^{} x (x \in (A \cup B) \land φ)$
3		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
4	3	anbi1i	$⊢ (x \in (A \cup B) \land φ) \leftrightarrow ((x \in A \lor x \in B) \land φ)$
5		andir	$⊢ ((x \in A \lor x \in B) \land φ) \leftrightarrow ((x \in A \land φ) \lor (x \in B \land φ))$
6	4 5	bitri	$⊢ (x \in (A \cup B) \land φ) \leftrightarrow ((x \in A \land φ) \lor (x \in B \land φ))$
7	6	mobii	$⊢ \exists^{} x (x \in (A \cup B) \land φ) \leftrightarrow \exists^{} x ((x \in A \land φ) \lor (x \in B \land φ))$
8	2 7	bitri	$⊢ \exists^{} x \in (A \cup B) φ \leftrightarrow \exists^{} x ((x \in A \land φ) \lor (x \in B \land φ))$
9		df-rmo	$⊢ \exists^{} x \in A φ \leftrightarrow \exists^{} x (x \in A \land φ)$
10		df-rmo	$⊢ \exists^{} x \in B φ \leftrightarrow \exists^{} x (x \in B \land φ)$
11	9 10	anbi12i	$⊢ (\exists^{} x \in A φ \land \exists^{} x \in B φ) \leftrightarrow (\exists^{} x (x \in A \land φ) \land \exists^{} x (x \in B \land φ))$
12	1 8 11	3imtr4i	$⊢ \exists^{} x \in (A \cup B) φ \to (\exists^{} x \in A φ \land \exists^{*} x \in B φ)$