![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.41 | Structured version Visualization version GIF version |
Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1953 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 |
---|---|
19.41.1 | ⊢ Ⅎ𝑥𝜓 |
Ref | Expression |
---|---|
19.41 | ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.40 1889 | . . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | |
2 | 19.41.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
3 | 2 | 19.9 2198 | . . . 4 ⊢ (∃𝑥𝜓 ↔ 𝜓) |
4 | 3 | anbi2i 623 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
5 | 1, 4 | sylib 217 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
6 | pm3.21 472 | . . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) | |
7 | 2, 6 | eximd 2209 | . . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) |
8 | 7 | impcom 408 | . 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 208 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∃wex 1781 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-nf 1786 |
This theorem is referenced by: 19.42 2229 eean 2344 eeeanv 2346 equsexALT 2418 2sb5rf 2471 r19.41 3260 eliunxp 5837 dfopab2 8037 dfoprab3s 8038 xpcomco 9061 mpomptxf 31900 bnj605 33913 bnj607 33922 2sb5nd 43311 2sb5ndVD 43661 2sb5ndALT 43683 eliunxp2 46999 |
Copyright terms: Public domain | W3C validator |