Theorem amosym1

Description: A symmetry with E* .

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

	Ref	Expression
Assertion	amosym1	⊢ ( ∃* 𝑥 ∃* 𝑥 ⊥ → ∃* 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		moeu	⊢ ( ∃* 𝑥 ∃* 𝑥 ⊥ ↔ ( ∃ 𝑥 ∃* 𝑥 ⊥ → ∃! 𝑥 ∃* 𝑥 ⊥ ) )
2		mofal	⊢ ∃* 𝑥 ⊥
3		19.8a	⊢ ( ∃* 𝑥 ⊥ → ∃ 𝑥 ∃* 𝑥 ⊥ )
4	3	notnotd	⊢ ( ∃* 𝑥 ⊥ → ¬ ¬ ∃ 𝑥 ∃* 𝑥 ⊥ )
5	2 4	ax-mp	⊢ ¬ ¬ ∃ 𝑥 ∃* 𝑥 ⊥
6	5	pm2.21i	⊢ ( ¬ ∃ 𝑥 ∃* 𝑥 ⊥ → ∃* 𝑥 𝜑 )
7	2	notnoti	⊢ ¬ ¬ ∃* 𝑥 ⊥
8	7	nex	⊢ ¬ ∃ 𝑥 ¬ ∃* 𝑥 ⊥
9		eunex	⊢ ( ∃! 𝑥 ∃* 𝑥 ⊥ → ∃ 𝑥 ¬ ∃* 𝑥 ⊥ )
10	8 9	mto	⊢ ¬ ∃! 𝑥 ∃* 𝑥 ⊥
11	10	pm2.21i	⊢ ( ∃! 𝑥 ∃* 𝑥 ⊥ → ∃* 𝑥 𝜑 )
12	6 11	ja	⊢ ( ( ∃ 𝑥 ∃* 𝑥 ⊥ → ∃! 𝑥 ∃* 𝑥 ⊥ ) → ∃* 𝑥 𝜑 )
13	1 12	sylbi	⊢ ( ∃* 𝑥 ∃* 𝑥 ⊥ → ∃* 𝑥 𝜑 )