Metamath Proof Explorer

Theorem reuun2

Description: Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005)

		Ref	Expression
	Assertion	reuun2	$⊢ \neg \exists x \in B φ \to (\exists! x \in (A \cup B) φ \leftrightarrow \exists! x \in A φ)$

Proof

Step	Hyp	Ref	Expression
1		df-rex	$⊢ \exists x \in B φ \leftrightarrow \exists x (x \in B \land φ)$
2		euor2	$⊢ \neg \exists x (x \in B \land φ) \to (\exists! x ((x \in B \land φ) \lor (x \in A \land φ)) \leftrightarrow \exists! x (x \in A \land φ))$
3	1 2	sylnbi	$⊢ \neg \exists x \in B φ \to (\exists! x ((x \in B \land φ) \lor (x \in A \land φ)) \leftrightarrow \exists! x (x \in A \land φ))$
4		df-reu	$⊢ \exists! x \in (A \cup B) φ \leftrightarrow \exists! x (x \in (A \cup B) \land φ)$
5		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
6	5	anbi1i	$⊢ (x \in (A \cup B) \land φ) \leftrightarrow ((x \in A \lor x \in B) \land φ)$
7		andir	$⊢ ((x \in A \lor x \in B) \land φ) \leftrightarrow ((x \in A \land φ) \lor (x \in B \land φ))$
8		orcom	$⊢ ((x \in A \land φ) \lor (x \in B \land φ)) \leftrightarrow ((x \in B \land φ) \lor (x \in A \land φ))$
9	7 8	bitri	$⊢ ((x \in A \lor x \in B) \land φ) \leftrightarrow ((x \in B \land φ) \lor (x \in A \land φ))$
10	6 9	bitri	$⊢ (x \in (A \cup B) \land φ) \leftrightarrow ((x \in B \land φ) \lor (x \in A \land φ))$
11	10	eubii	$⊢ \exists! x (x \in (A \cup B) \land φ) \leftrightarrow \exists! x ((x \in B \land φ) \lor (x \in A \land φ))$
12	4 11	bitri	$⊢ \exists! x \in (A \cup B) φ \leftrightarrow \exists! x ((x \in B \land φ) \lor (x \in A \land φ))$
13		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
14	3 12 13	3bitr4g	$⊢ \neg \exists x \in B φ \to (\exists! x \in (A \cup B) φ \leftrightarrow \exists! x \in A φ)$