|   | 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 1847 | . . 3 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ ∃𝑥(¬ 𝜑 → 𝜓)) | 
| 3 | 19.35 1876 | . . 3 ⊢ (∃𝑥(¬ 𝜑 → 𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓)) | |
| 4 | alnex 1780 | . . . 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 1537 ∃wex 1778 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-or 848 df-ex 1779 | 
| This theorem is referenced by: 19.34 1985 19.44v 1991 19.45v 1992 19.44 2236 19.45 2237 eeor 2334 rexun 4195 uniprg 4922 uniun 4929 unopab 5223 zfpair 5420 dmun 5920 dmopab2rex 5927 coundi 6266 coundir 6267 kmlem16 10207 vdwapun 17013 satfdm 35375 satf0op 35383 dmopab3rexdif 35411 bj-nnfor 36752 bj-nnford 36753 exor 42682 pm10.42 44388 | 
| Copyright terms: Public domain | W3C validator |