Theorem bj-modal4e

Description: First-order logic form of the modal axiom (4) using existential quantifiers. Dual statement of bj-modal4 ( hba1 ). (Contributed by BJ, 21-Dec-2020) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-modal4e	⊢ ( ∃ 𝑥 ∃ 𝑥 𝜑 → ∃ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		bj-modal4	⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 )
2		alnex	⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
3		2exnaln	⊢ ( ∃ 𝑥 ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 )
4	3	con2bii	⊢ ( ∀ 𝑥 ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 ∃ 𝑥 𝜑 )
5	1 2 4	3imtr3i	⊢ ( ¬ ∃ 𝑥 𝜑 → ¬ ∃ 𝑥 ∃ 𝑥 𝜑 )
6	5	con4i	⊢ ( ∃ 𝑥 ∃ 𝑥 𝜑 → ∃ 𝑥 𝜑 )