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

Proof

Step	Hyp	Ref	Expression
1		reuimrmo	|- ( A. x e. A ( E! y e. B ph -> E* y e. B ph ) -> ( E! x e. A E* y e. B ph -> E* x e. A E! y e. B ph ) )
2		reurmo	|- ( E! y e. B ph -> E* y e. B ph )
3	2	a1i	|- ( x e. A -> ( E! y e. B ph -> E* y e. B ph ) )
4	1 3	mprg	|- ( E! x e. A E* y e. B ph -> E* x e. A E! y e. B ph )