Metamath Proof Explorer


Theorem 19.41

Description: Theorem 19.41 of Margaris p. 90. See 19.41v for a version requiring fewer axioms. (Contributed by NM, 14-May-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 12-Jan-2018)

Ref Expression
Hypothesis 19.41.1 𝑥 𝜓
Assertion 19.41 ( ∃ 𝑥 ( 𝜑𝜓 ) ↔ ( ∃ 𝑥 𝜑𝜓 ) )

Proof

Step Hyp Ref Expression
1 19.41.1 𝑥 𝜓
2 19.40 ( ∃ 𝑥 ( 𝜑𝜓 ) → ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) )
3 1 19.9 ( ∃ 𝑥 𝜓𝜓 )
4 3 anbi2i ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) ↔ ( ∃ 𝑥 𝜑𝜓 ) )
5 2 4 sylib ( ∃ 𝑥 ( 𝜑𝜓 ) → ( ∃ 𝑥 𝜑𝜓 ) )
6 pm3.21 ( 𝜓 → ( 𝜑 → ( 𝜑𝜓 ) ) )
7 1 6 eximd ( 𝜓 → ( ∃ 𝑥 𝜑 → ∃ 𝑥 ( 𝜑𝜓 ) ) )
8 7 impcom ( ( ∃ 𝑥 𝜑𝜓 ) → ∃ 𝑥 ( 𝜑𝜓 ) )
9 5 8 impbii ( ∃ 𝑥 ( 𝜑𝜓 ) ↔ ( ∃ 𝑥 𝜑𝜓 ) )