Theorem 2reurex

Description: Double restricted quantification with existential uniqueness, analogous to 2euex . (Contributed by Alexander van der Vekens, 24-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		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 ) )
2		rexcom	|- ( E. x e. A E. y e. B ph <-> E. y e. B E. x e. A ph )
3		nfcv	|- F/_ y A
4		nfre1	|- F/ y E. y e. B ph
5	3 4	nfrmow	|- F/ y E* x e. A E. y e. B ph
6		rspe	|- ( ( y e. B /\ ph ) -> E. y e. B ph )
7	6	ex	|- ( y e. B -> ( ph -> E. y e. B ph ) )
8	7	ralrimivw	|- ( y e. B -> A. x e. A ( ph -> E. y e. B ph ) )
9		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 ) )
10	8 9	syl	|- ( y e. B -> ( E* x e. A E. y e. B ph -> E* x e. A ph ) )
11	10	impcom	|- ( ( E* x e. A E. y e. B ph /\ y e. B ) -> E* x e. A ph )
12		rmo5	|- ( E* x e. A ph <-> ( E. x e. A ph -> E! x e. A ph ) )
13	11 12	sylib	|- ( ( E* x e. A E. y e. B ph /\ y e. B ) -> ( E. x e. A ph -> E! x e. A ph ) )
14	13	ex	|- ( E* x e. A E. y e. B ph -> ( y e. B -> ( E. x e. A ph -> E! x e. A ph ) ) )
15	5 14	reximdai	|- ( E* x e. A E. y e. B ph -> ( E. y e. B E. x e. A ph -> E. y e. B E! x e. A ph ) )
16	2 15	biimtrid	|- ( E* x e. A E. y e. B ph -> ( E. x e. A E. y e. B ph -> E. y e. B E! x e. A ph ) )
17	16	impcom	|- ( ( E. x e. A E. y e. B ph /\ E* x e. A E. y e. B ph ) -> E. y e. B E! x e. A ph )
18	1 17	sylbi	|- ( E! x e. A E. y e. B ph -> E. y e. B E! x e. A ph )