![]() |
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 1947 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 1884 | . . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | |
2 | 19.41.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
3 | 2 | 19.9 2203 | . . . 4 ⊢ (∃𝑥𝜓 ↔ 𝜓) |
4 | 3 | anbi2i 623 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
5 | 1, 4 | sylib 218 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
6 | pm3.21 471 | . . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) | |
7 | 2, 6 | eximd 2214 | . . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) |
8 | 7 | impcom 407 | . 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 209 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1776 Ⅎwnf 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-nf 1781 |
This theorem is referenced by: 19.42 2234 eean 2349 eeeanv 2351 equsexALT 2422 2sb5rf 2475 r19.41 3261 eliunxp 5851 dfopab2 8076 dfoprab3s 8077 xpcomco 9101 mpomptxf 32694 bnj605 34900 bnj607 34909 2sb5nd 44558 2sb5ndVD 44908 2sb5ndALT 44930 eliunxp2 48179 |
Copyright terms: Public domain | W3C validator |