Theorem 2reucom

Description: Double restricted existential uniqueness commutes. (Contributed by Thierry Arnoux, 4-Jul-2023)

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

Proof

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