![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > r19.43 | Structured version Visualization version GIF version |
Description: Restricted quantifier version of 19.43 1886. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
Ref | Expression |
---|---|
r19.43 | ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.35 3109 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | |
2 | df-or 847 | . . 3 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
3 | 2 | rexbii 3095 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓)) |
4 | df-or 847 | . . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | |
5 | ralnex 3073 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
6 | 5 | imbi1i 350 | . . 3 ⊢ ((∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
7 | 4, 6 | bitr4i 278 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
8 | 1, 3, 7 | 3bitr4i 303 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∨ wo 846 ∀wral 3062 ∃wrex 3071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-ral 3063 df-rex 3072 |
This theorem is referenced by: r19.45v 3193 r19.44v 3194 r19.45zv 4503 r19.44zv 4504 iunun 5097 soseq 8145 wemapsolem 9545 pythagtriplem2 16750 pythagtrip 16767 dcubic 26351 addsdilem1 27609 mulsasslem2 27622 legtrid 27873 axcontlem4 28256 erdszelem11 34223 satfvsucsuc 34387 fmla1 34409 seglelin 35119 diophun 41559 rexzrexnn0 41590 ldepslinc 47238 |
Copyright terms: Public domain | W3C validator |