|   | 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 1881. (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 3107 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | |
| 2 | df-or 848 | . . 3 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
| 3 | 2 | rexbii 3093 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓)) | 
| 4 | df-or 848 | . . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | |
| 5 | ralnex 3071 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
| 6 | 5 | imbi1i 349 | . . 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 206 ∨ wo 847 ∀wral 3060 ∃wrex 3069 | 
| 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-an 396 df-or 848 df-ex 1779 df-ral 3061 df-rex 3070 | 
| This theorem is referenced by: r19.45v 3192 r19.44v 3193 r19.45zv 4502 r19.44zv 4503 iunun 5092 soseq 8185 wemapsolem 9591 pythagtriplem2 16856 pythagtrip 16873 dcubic 26890 addsdilem1 28178 mulsasslem2 28191 legtrid 28600 axcontlem4 28983 erdszelem11 35207 satfvsucsuc 35371 fmla1 35393 seglelin 36118 hashnexinjle 42131 fimgmcyclem 42548 rexor 42683 diophun 42789 rexzrexnn0 42820 dfvopnbgr2 47844 dfsclnbgr6 47849 ldepslinc 48431 | 
| Copyright terms: Public domain | W3C validator |