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 842 | . . . 4 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
2 | 1 | exbii 1839 | . . 3 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ ∃𝑥(¬ 𝜑 → 𝜓)) |
3 | 19.35 1869 | . . 3 ⊢ (∃𝑥(¬ 𝜑 → 𝜓) ↔ (∀𝑥 ¬ 𝜑 → ∃𝑥𝜓)) | |
4 | alnex 1773 | . . . 4 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) | |
5 | 4 | imbi1i 351 | . . 3 ⊢ ((∀𝑥 ¬ 𝜑 → ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓)) |
6 | 2, 3, 5 | 3bitri 298 | . 2 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓)) |
7 | df-or 842 | . 2 ⊢ ((∃𝑥𝜑 ∨ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 → ∃𝑥𝜓)) | |
8 | 6, 7 | bitr4i 279 | 1 ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∨ wo 841 ∀wal 1526 ∃wex 1771 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-or 842 df-ex 1772 |
This theorem is referenced by: 19.34 1984 19.44v 1990 19.45v 1991 19.44 2229 19.45 2230 rexun 4163 unipr 4843 uniun 4849 unopab 5136 zfpair 5312 dmun 5772 dmopab2rex 5779 coundi 6093 coundir 6094 kmlem16 9579 vdwapun 16298 satfdm 32513 satf0op 32521 dmopab3rexdif 32549 bj-nnfor 33976 bj-nnford 33977 pm10.42 40573 |
Copyright terms: Public domain | W3C validator |