Metamath Proof Explorer


Theorem 19.41v

Description: Version of 19.41 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)

Ref Expression
Assertion 19.41v ( ∃ 𝑥 ( 𝜑𝜓 ) ↔ ( ∃ 𝑥 𝜑𝜓 ) )

Proof

Step Hyp Ref Expression
1 19.40 ( ∃ 𝑥 ( 𝜑𝜓 ) → ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) )
2 ax5e ( ∃ 𝑥 𝜓𝜓 )
3 2 anim2i ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) → ( ∃ 𝑥 𝜑𝜓 ) )
4 1 3 syl ( ∃ 𝑥 ( 𝜑𝜓 ) → ( ∃ 𝑥 𝜑𝜓 ) )
5 pm3.21 ( 𝜓 → ( 𝜑 → ( 𝜑𝜓 ) ) )
6 5 eximdv ( 𝜓 → ( ∃ 𝑥 𝜑 → ∃ 𝑥 ( 𝜑𝜓 ) ) )
7 6 impcom ( ( ∃ 𝑥 𝜑𝜓 ) → ∃ 𝑥 ( 𝜑𝜓 ) )
8 4 7 impbii ( ∃ 𝑥 ( 𝜑𝜓 ) ↔ ( ∃ 𝑥 𝜑𝜓 ) )