![]() |
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 1878. (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 3098 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | |
2 | df-or 846 | . . 3 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
3 | 2 | rexbii 3084 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓)) |
4 | df-or 846 | . . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | |
5 | ralnex 3062 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
6 | 5 | imbi1i 348 | . . 3 ⊢ ((∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
7 | 4, 6 | bitr4i 277 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
8 | 1, 3, 7 | 3bitr4i 302 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∨ wo 845 ∀wral 3051 ∃wrex 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1775 df-ral 3052 df-rex 3061 |
This theorem is referenced by: r19.45v 3183 r19.44v 3184 r19.45zv 4497 r19.44zv 4498 iunun 5093 soseq 8165 wemapsolem 9586 pythagtriplem2 16814 pythagtrip 16831 dcubic 26871 addsdilem1 28149 mulsasslem2 28162 legtrid 28515 axcontlem4 28898 erdszelem11 35042 satfvsucsuc 35206 fmla1 35228 seglelin 35953 hashnexinjle 41841 fimgmcyclem 42223 rexor 42357 diophun 42467 rexzrexnn0 42498 dfvopnbgr2 47456 dfsclnbgr6 47461 ldepslinc 47928 |
Copyright terms: Public domain | W3C validator |