![]() |
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 2029 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 1948 | . . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | |
2 | 19.41.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
3 | 2 | 19.9 2228 | . . . 4 ⊢ (∃𝑥𝜓 ↔ 𝜓) |
4 | 3 | anbi2i 609 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
5 | 1, 4 | sylib 208 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
6 | pm3.21 448 | . . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) | |
7 | 2, 6 | eximd 2241 | . . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) |
8 | 7 | impcom 394 | . 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 199 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 382 ∃wex 1852 Ⅎwnf 1856 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-12 2203 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 df-nf 1858 |
This theorem is referenced by: 19.42 2261 equsexv 2265 eean 2343 eeeanv 2345 equsexALT 2448 2sb5rf 2599 r19.41 3238 eliunxp 5398 dfopab2 7371 dfoprab3s 7372 xpcomco 8206 mpt2mptxf 29817 bnj605 31315 bnj607 31324 2sb5nd 39301 2sb5ndVD 39668 2sb5ndALT 39690 eliunxp2 42640 |
Copyright terms: Public domain | W3C validator |