Theorem unqsym1

Description: A symmetry with E! .

See negsym1 for more information. (Contributed by Anthony Hart, 6-Sep-2011)

	Ref	Expression
Assertion	unqsym1	|- ( E! x E! x F. -> E! x ph )

Proof

Step	Hyp	Ref	Expression
1		neufal	|- -. E! x F.
2	1	nex	|- -. E. x E! x F.
3		euex	|- ( E! x E! x F. -> E. x E! x F. )
4	2 3	mto	|- -. E! x E! x F.
5	4	pm2.21i	|- ( E! x E! x F. -> E! x ph )