Theorem 2rexreu

Description: Double restricted existential uniqueness implies double restricted unique existential quantification, analogous to 2exeu . (Contributed by Alexander van der Vekens, 25-Jun-2017)

	Ref	Expression
Assertion	2rexreu	|- ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) -> E! x e. A E! y e. B ph )

Proof

Step	Hyp	Ref	Expression
1		reurmo	|- ( E! x e. A E. y e. B ph -> E* x e. A E. y e. B ph )
2		reurex	|- ( E! y e. B ph -> E. y e. B ph )
3	2	rmoimi	|- ( E* x e. A E. y e. B ph -> E* x e. A E! y e. B ph )
4	1 3	syl	|- ( E! x e. A E. y e. B ph -> E* x e. A E! y e. B ph )
5		2reurex	|- ( E! y e. B E. x e. A ph -> E. x e. A E! y e. B ph )
6	4 5	anim12ci	|- ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) -> ( E. x e. A E! y e. B ph /\ E* x e. A E! y e. B ph ) )
7		reu5	|- ( E! x e. A E! y e. B ph <-> ( E. x e. A E! y e. B ph /\ E* x e. A E! y e. B ph ) )
8	6 7	sylibr	|- ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) -> E! x e. A E! y e. B ph )