Theorem reuss

Description: Transfer uniqueness to a smaller subclass. (Contributed by NM, 21-Aug-1999)

	Ref	Expression
Assertion	reuss	$$⊢\left(A\subseteq B\wedge \exists x\in A\phi \wedge \exists !x\in B\phi \right)\to \exists !x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢\phi \to \phi$$
2	1	rgenw	$$⊢\forall x\in A\left(\phi \to \phi \right)$$
3		reuss2	$$⊢\left(\left(A\subseteq B\wedge \forall x\in A\left(\phi \to \phi \right)\right)\wedge \left(\exists x\in A\phi \wedge \exists !x\in B\phi \right)\right)\to \exists !x\in A\phi$$
4	2 3	mpanl2	$$⊢\left(A\subseteq B\wedge \left(\exists x\in A\phi \wedge \exists !x\in B\phi \right)\right)\to \exists !x\in A\phi$$
5	4	3impb	$$⊢\left(A\subseteq B\wedge \exists x\in A\phi \wedge \exists !x\in B\phi \right)\to \exists !x\in A\phi$$