Metamath Proof Explorer

Theorem 2reu2reu2

Description: Double restricted existential uniqueness implies two nested restricted existential uniqueness. (Contributed by AV, 5-Jul-2023)

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

Step	Hyp	Ref	Expression
1		df-2reu	\|- ( E! x e. A , y e. B ph <-> ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) )
2		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 )
3	1 2	sylbi	\|- ( E! x e. A , y e. B ph -> E! x e. A E! y e. B ph )

Step

Hyp

Ref

Expression

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

1 2

 |-  ( E! x e. A , y e. B ph -> E! x e. A E! y e. B ph )