Theorem 2reurmo

Description: Double restricted quantification with restricted existential uniqueness and restricted "at most one", analogous to 2eumo . (Contributed by Alexander van der Vekens, 24-Jun-2017)

	Ref	Expression
Assertion	2reurmo	$$⊢\exists !x\in A{\exists }^{*}y\in B\phi \to {\exists }^{*}x\in A\exists !y\in B\phi$$

Proof

Step	Hyp	Ref	Expression
1		reuimrmo	$$⊢\forall x\in A\left(\exists !y\in B\phi \to {\exists }^{*}y\in B\phi \right)\to \left(\exists !x\in A{\exists }^{*}y\in B\phi \to {\exists }^{*}x\in A\exists !y\in B\phi \right)$$
2		reurmo	$$⊢\exists !y\in B\phi \to {\exists }^{*}y\in B\phi$$
3	2	a1i	$$⊢x\in A\to \left(\exists !y\in B\phi \to {\exists }^{*}y\in B\phi \right)$$
4	1 3	mprg	$$⊢\exists !x\in A{\exists }^{*}y\in B\phi \to {\exists }^{*}x\in A\exists !y\in B\phi$$