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	|- ( E* x e. A E. y e. B ph -> A. y e. B E* x e. A ph )

Proof

Step	Hyp	Ref	Expression
1		nfcv	|- F/_ y A
2		nfre1	|- F/ y E. y e. B ph
3	1 2	nfrmow	|- F/ y E* x e. A E. y e. B ph
4		rmoim	|- ( A. x e. A ( ph -> E. y e. B ph ) -> ( E* x e. A E. y e. B ph -> E* x e. A ph ) )
5		rspe	|- ( ( y e. B /\ ph ) -> E. y e. B ph )
6	5	ex	|- ( y e. B -> ( ph -> E. y e. B ph ) )
7	6	ralrimivw	|- ( y e. B -> A. x e. A ( ph -> E. y e. B ph ) )
8	4 7	syl11	|- ( E* x e. A E. y e. B ph -> ( y e. B -> E* x e. A ph ) )
9	3 8	ralrimi	|- ( E* x e. A E. y e. B ph -> A. y e. B E* x e. A ph )