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

Metamath Proof Explorer

Theorem bj-19.42t

Description: Closed form of 19.42 from the same axioms as 19.42v . (Contributed by BJ, 2-Dec-2023)

Ref Expression
Assertion bj-19.42t ( Ⅎ' 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃ 𝑥 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 19.40 ⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) )
2 bj-nnfe ⊢ ( Ⅎ' 𝑥 𝜑 → ( ∃ 𝑥 𝜑 → 𝜑 ) )
3 2 anim1d ⊢ ( Ⅎ' 𝑥 𝜑 → ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) → ( 𝜑 ∧ ∃ 𝑥 𝜓 ) ) )
4 1 3 syl5 ⊢ ( Ⅎ' 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ ∃ 𝑥 𝜓 ) ) )
5 bj-nnfa ⊢ ( Ⅎ' 𝑥 𝜑 → ( 𝜑 → ∀ 𝑥 𝜑 ) )
6 5 anim1d ⊢ ( Ⅎ' 𝑥 𝜑 → ( ( 𝜑 ∧ ∃ 𝑥 𝜓 ) → ( ∀ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) ) )
7 19.29 ⊢ ( ( ∀ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )
8 6 7 syl6 ⊢ ( Ⅎ' 𝑥 𝜑 → ( ( 𝜑 ∧ ∃ 𝑥 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) )
9 4 8 impbid ⊢ ( Ⅎ' 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃ 𝑥 𝜓 ) ) )