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 1799. (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 3065 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | |
2 | df-or 384 | . . 3 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
3 | 2 | rexbii 3023 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓)) |
4 | df-or 384 | . . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | |
5 | ralnex 2975 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
6 | 5 | imbi1i 338 | . . 3 ⊢ ((∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
7 | 4, 6 | bitr4i 266 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
8 | 1, 3, 7 | 3bitr4i 291 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∀wral 2896 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-ex 1696 df-ral 2901 df-rex 2902 |
This theorem is referenced by: r19.44v 3075 r19.45v 3076 r19.45zv 4020 r19.44zv 4021 iunun 4540 wemapsolem 8338 pythagtriplem2 15360 pythagtrip 15377 dcubic 24373 legtrid 25286 axcontlem4 25647 erdszelem11 30437 soseq 30995 seglelin 31393 diophun 36355 rexzrexnn0 36386 ldepslinc 42092 |
Copyright terms: Public domain | W3C validator |