Theorem unqsym1

Description: A symmetry with E! .

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

	Ref	Expression
Assertion	unqsym1	$$⊢\exists !x\exists !x\perp \to \exists !x\phi$$

Proof

Step	Hyp	Ref	Expression
1		neufal	$$⊢\neg \exists !x\perp$$
2	1	nex	$$⊢\neg \exists x\exists !x\perp$$
3		euex	$$⊢\exists !x\exists !x\perp \to \exists x\exists !x\perp$$
4	2 3	mto	$$⊢\neg \exists !x\exists !x\perp$$
5	4	pm2.21i	$$⊢\exists !x\exists !x\perp \to \exists !x\phi$$