Theorem reuun1

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

	Ref	Expression
Assertion	reuun1	$$⊢\left(\exists x\in A\phi \wedge \exists !x\in \left(A\cup B\right)\left(\phi \vee \psi \right)\right)\to \exists !x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		ssun1	$$⊢A\subseteq A\cup B$$
2		orc	$$⊢\phi \to \left(\phi \vee \psi \right)$$
3	2	rgenw	$$⊢\forall x\in A\left(\phi \to \left(\phi \vee \psi \right)\right)$$
4		reuss2	$$⊢\left(\left(A\subseteq A\cup B\wedge \forall x\in A\left(\phi \to \left(\phi \vee \psi \right)\right)\right)\wedge \left(\exists x\in A\phi \wedge \exists !x\in \left(A\cup B\right)\left(\phi \vee \psi \right)\right)\right)\to \exists !x\in A\phi$$
5	1 3 4	mpanl12	$$⊢\left(\exists x\in A\phi \wedge \exists !x\in \left(A\cup B\right)\left(\phi \vee \psi \right)\right)\to \exists !x\in A\phi$$