Metamath Proof Explorer

Theorem rmounid

Description: A case where an "at most one" restricted existential quantifier for a union is equivalent to such a quantifier for one of the sets. (Contributed by Thierry Arnoux, 27-Nov-2023)

		Ref	Expression
	Hypothesis	rmounid.1	$⊢ (φ \land x \in B) \to \neg ψ$
	Assertion	rmounid	$⊢ φ \to (\exists^{} x \in (A \cup B) ψ \leftrightarrow \exists^{} x \in A ψ)$

Proof

Step	Hyp	Ref	Expression
1		rmounid.1	$⊢ (φ \land x \in B) \to \neg ψ$
2	1	ex	$⊢ φ \to (x \in B \to \neg ψ)$
3	2	con2d	$⊢ φ \to (ψ \to \neg x \in B)$
4	3	imp	$⊢ (φ \land ψ) \to \neg x \in B$
5		biorf	$⊢ \neg x \in B \to (x \in A \leftrightarrow (x \in B \lor x \in A))$
6		orcom	$⊢ (x \in A \lor x \in B) \leftrightarrow (x \in B \lor x \in A)$
7	5 6	bitr4di	$⊢ \neg x \in B \to (x \in A \leftrightarrow (x \in A \lor x \in B))$
8	4 7	syl	$⊢ (φ \land ψ) \to (x \in A \leftrightarrow (x \in A \lor x \in B))$
9		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
10	8 9	bitr4di	$⊢ (φ \land ψ) \to (x \in A \leftrightarrow x \in (A \cup B))$
11	10	pm5.32da	$⊢ φ \to ((ψ \land x \in A) \leftrightarrow (ψ \land x \in (A \cup B)))$
12	11	biancomd	$⊢ φ \to ((ψ \land x \in A) \leftrightarrow (x \in (A \cup B) \land ψ))$
13	12	bicomd	$⊢ φ \to ((x \in (A \cup B) \land ψ) \leftrightarrow (ψ \land x \in A))$
14	13	biancomd	$⊢ φ \to ((x \in (A \cup B) \land ψ) \leftrightarrow (x \in A \land ψ))$
15	14	mobidv	$⊢ φ \to (\exists^{} x (x \in (A \cup B) \land ψ) \leftrightarrow \exists^{} x (x \in A \land ψ))$
16		df-rmo	$⊢ \exists^{} x \in (A \cup B) ψ \leftrightarrow \exists^{} x (x \in (A \cup B) \land ψ)$
17		df-rmo	$⊢ \exists^{} x \in A ψ \leftrightarrow \exists^{} x (x \in A \land ψ)$
18	15 16 17	3bitr4g	$⊢ φ \to (\exists^{} x \in (A \cup B) ψ \leftrightarrow \exists^{} x \in A ψ)$