Theorem unqsym1

Description: A symmetry with E! .

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

	Ref	Expression
Assertion	unqsym1	⊢ ( ∃! 𝑥 ∃! 𝑥 ⊥ → ∃! 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		neufal	⊢ ¬ ∃! 𝑥 ⊥
2	1	nex	⊢ ¬ ∃ 𝑥 ∃! 𝑥 ⊥
3		euex	⊢ ( ∃! 𝑥 ∃! 𝑥 ⊥ → ∃ 𝑥 ∃! 𝑥 ⊥ )
4	2 3	mto	⊢ ¬ ∃! 𝑥 ∃! 𝑥 ⊥
5	4	pm2.21i	⊢ ( ∃! 𝑥 ∃! 𝑥 ⊥ → ∃! 𝑥 𝜑 )