Theorem 2eu2

Description: Double existential uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Dec-2001) (New usage is discouraged.)

	Ref	Expression
Assertion	2eu2	|- ( E! y E. x ph -> ( E! x E! y ph <-> E! x E. y ph ) )

Proof

Step	Hyp	Ref	Expression
1		eumo	|- ( E! y E. x ph -> E* y E. x ph )
2		2moex	|- ( E* y E. x ph -> A. x E* y ph )
3		2eu1	|- ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) )
4		simpl	|- ( ( E! x E. y ph /\ E! y E. x ph ) -> E! x E. y ph )
5	3 4	biimtrdi	|- ( A. x E* y ph -> ( E! x E! y ph -> E! x E. y ph ) )
6	1 2 5	3syl	|- ( E! y E. x ph -> ( E! x E! y ph -> E! x E. y ph ) )
7		2exeu	|- ( ( E! x E. y ph /\ E! y E. x ph ) -> E! x E! y ph )
8	7	expcom	|- ( E! y E. x ph -> ( E! x E. y ph -> E! x E! y ph ) )
9	6 8	impbid	|- ( E! y E. x ph -> ( E! x E! y ph <-> E! x E. y ph ) )