Theorem 2rmorex

Description: Double restricted quantification with "at most one", analogous to 2moex . (Contributed by Alexander van der Vekens, 17-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
2		nfre1	$$⊢Ⅎy\exists y\in B\phi$$
3	1 2	nfrmow	$$⊢Ⅎy{\exists }^{*}x\in A\exists y\in B\phi$$
4		rmoim	$$⊢\forall x\in A\left(\phi \to \exists y\in B\phi \right)\to \left({\exists }^{*}x\in A\exists y\in B\phi \to {\exists }^{*}x\in A\phi \right)$$
5		rspe	$$⊢\left(y\in B\wedge \phi \right)\to \exists y\in B\phi$$
6	5	ex	$$⊢y\in B\to \left(\phi \to \exists y\in B\phi \right)$$
7	6	ralrimivw	$$⊢y\in B\to \forall x\in A\left(\phi \to \exists y\in B\phi \right)$$
8	4 7	syl11	$$⊢{\exists }^{*}x\in A\exists y\in B\phi \to \left(y\in B\to {\exists }^{*}x\in A\phi \right)$$
9	3 8	ralrimi	$$⊢{\exists }^{*}x\in A\exists y\in B\phi \to \forall y\in B{\exists }^{*}x\in A\phi$$