|   | 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 1948 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 1885 | . . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | |
| 2 | 19.41.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
| 3 | 2 | 19.9 2204 | . . . 4 ⊢ (∃𝑥𝜓 ↔ 𝜓) | 
| 4 | 3 | anbi2i 623 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) | 
| 5 | 1, 4 | sylib 218 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓)) | 
| 6 | pm3.21 471 | . . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) | |
| 7 | 2, 6 | eximd 2215 | . . 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 1778 Ⅎwnf 1782 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-nf 1783 | 
| This theorem is referenced by: 19.42 2235 eean 2349 eeeanv 2351 equsexALT 2423 2sb5rf 2476 r19.41 3262 eliunxp 5847 dfopab2 8078 dfoprab3s 8079 xpcomco 9103 mpomptxf 32688 bnj605 34922 bnj607 34931 2sb5nd 44585 2sb5ndVD 44935 2sb5ndALT 44957 eliunxp2 48255 | 
| Copyright terms: Public domain | W3C validator |