Theorem 2reu7

Description: Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 . (Contributed by Alexander van der Vekens, 2-Jul-2017)

	Ref	Expression
Assertion	2reu7	|- ( ( 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 ( E. x e. A ph /\ E. y e. B ph ) )

Proof

Step	Hyp	Ref	Expression
1		nfcv	|- F/_ x B
2		nfre1	|- F/ x E. x e. A ph
3	1 2	nfreuw	|- F/ x E! y e. B E. x e. A ph
4	3	reuan	|- ( E! x e. A ( E! y e. B E. x e. A ph /\ E. y e. B ph ) <-> ( E! y e. B E. x e. A ph /\ E! x e. A E. y e. B ph ) )
5		ancom	|- ( ( E. x e. A ph /\ E. y e. B ph ) <-> ( E. y e. B ph /\ E. x e. A ph ) )
6	5	reubii	|- ( E! y e. B ( E. x e. A ph /\ E. y e. B ph ) <-> E! y e. B ( E. y e. B ph /\ E. x e. A ph ) )
7		nfre1	|- F/ y E. y e. B ph
8	7	reuan	|- ( E! y e. B ( E. y e. B ph /\ E. x e. A ph ) <-> ( E. y e. B ph /\ E! y e. B E. x e. A ph ) )
9		ancom	|- ( ( E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( E! y e. B E. x e. A ph /\ E. y e. B ph ) )
10	6 8 9	3bitri	|- ( E! y e. B ( E. x e. A ph /\ E. y e. B ph ) <-> ( E! y e. B E. x e. A ph /\ E. y e. B ph ) )
11	10	reubii	|- ( E! x e. A E! y e. B ( E. x e. A ph /\ E. y e. B ph ) <-> E! x e. A ( E! y e. B E. x e. A ph /\ E. y e. B ph ) )
12		ancom	|- ( ( 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 /\ E! x e. A E. y e. B ph ) )
13	4 11 12	3bitr4ri	|- ( ( 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 ( E. x e. A ph /\ E. y e. B ph ) )