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 1901 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 1785 | . . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | |
2 | 19.41.1 | . . . . 5 ⊢ Ⅎ𝑥𝜓 | |
3 | 2 | 19.9 2060 | . . . 4 ⊢ (∃𝑥𝜓 ↔ 𝜓) |
4 | 3 | anbi2i 726 | . . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
5 | 1, 4 | sylib 207 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓)) |
6 | pm3.21 463 | . . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓))) | |
7 | 2, 6 | eximd 2072 | . . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) |
8 | 7 | impcom 445 | . 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 198 | 1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 ∃wex 1695 Ⅎwnf 1699 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-nf 1701 |
This theorem is referenced by: 19.42 2092 equsexv 2095 exanOLDOLD 2155 eean 2169 eeeanv 2171 equsexALT 2282 2sb5rf 2439 r19.41 3071 eliunxp 5181 dfopab2 7113 dfoprab3s 7114 xpcomco 7935 mpt2mptxf 28860 bnj605 30231 bnj607 30240 2sb5nd 37797 2sb5ndVD 38168 2sb5ndALT 38190 eliunxp2 41905 |
Copyright terms: Public domain | W3C validator |