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 | ⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∧ 𝜓 ) ) |
| 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 | ⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∧ 𝜓 ) ) |