This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-19.41al

Description: Special case of 19.41 proved from core axioms, ax-10 (modal5), and hba1 (modal4). (Contributed by BJ, 29-Dec-2020) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	bj-19.41al	⊢ ( ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑥 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		19.40	⊢ ( ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑥 𝜓 ) → ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 ∀ 𝑥 𝜓 ) )
2		hbe1a	⊢ ( ∃ 𝑥 ∀ 𝑥 𝜓 → ∀ 𝑥 𝜓 )
3	2	anim2i	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 ∀ 𝑥 𝜓 ) → ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) )
4	1 3	syl	⊢ ( ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑥 𝜓 ) → ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) )
5		hba1	⊢ ( ∀ 𝑥 𝜓 → ∀ 𝑥 ∀ 𝑥 𝜓 )
6	5	anim2i	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) → ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ∀ 𝑥 𝜓 ) )
7		19.29r	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 ∀ 𝑥 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑥 𝜓 ) )
8	6 7	syl	⊢ ( ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑥 𝜓 ) )
9	4 8	impbii	⊢ ( ∃ 𝑥 ( 𝜑 ∧ ∀ 𝑥 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∧ ∀ 𝑥 𝜓 ) )