Theorem 2reu5a

Description: Double restricted existential uniqueness in terms of restricted existence and restricted "at most one". (Contributed by Alexander van der Vekens, 17-Jun-2017)

	Ref	Expression
Assertion	2reu5a	|- ( E! x e. A E! y e. B ph <-> ( E. x e. A ( E. y e. B ph /\ E* y e. B ph ) /\ E* x e. A ( E. y e. B ph /\ E* y e. B 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		reu5	|- ( E! y e. B ph <-> ( E. y e. B ph /\ E* y e. B ph ) )
3	2	rexbii	|- ( E. x e. A E! y e. B ph <-> E. x e. A ( E. y e. B ph /\ E* y e. B ph ) )
4	2	rmobii	|- ( E* x e. A E! y e. B ph <-> E* x e. A ( E. y e. B ph /\ E* y e. B ph ) )
5	3 4	anbi12i	|- ( ( 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 /\ E* y e. B ph ) /\ E* x e. A ( E. y e. B ph /\ E* y e. B ph ) ) )
6	1 5	bitri	|- ( E! x e. A E! y e. B ph <-> ( E. x e. A ( E. y e. B ph /\ E* y e. B ph ) /\ E* x e. A ( E. y e. B ph /\ E* y e. B ph ) ) )