![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.43 | Structured version Visualization version GIF version |
Description: Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.) |
Ref | Expression |
---|---|
19.43 | ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-or 848 | . . . 4 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
2 | 1 | exbii 1845 | . . 3 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ ∃𝑥(¬ 𝜑 → 𝜓)) |
3 | 19.35 1875 | . . 3 ⊢ (∃𝑥(¬ 𝜑 → 𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓)) | |
4 | alnex 1778 | . . . 4 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) | |
5 | 4 | imbi1i 349 | . . 3 ⊢ ((∀𝑥 ¬ 𝜑 → ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓)) |
6 | 2, 3, 5 | 3bitri 297 | . 2 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓)) |
7 | df-or 848 | . 2 ⊢ ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓)) | |
8 | 6, 7 | bitr4i 278 | 1 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∨ wo 847 ∀wal 1535 ∃wex 1776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 207 df-or 848 df-ex 1777 |
This theorem is referenced by: 19.34 1984 19.44v 1990 19.45v 1991 19.44 2235 19.45 2236 eeor 2334 rexun 4206 uniprg 4928 uniun 4935 unopab 5230 zfpair 5427 dmun 5924 dmopab2rex 5931 coundi 6269 coundir 6270 kmlem16 10204 vdwapun 17008 satfdm 35354 satf0op 35362 dmopab3rexdif 35390 bj-nnfor 36733 bj-nnford 36734 exor 42654 pm10.42 44360 |
Copyright terms: Public domain | W3C validator |