![]() |
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 1850. (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 3113 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | |
2 | df-or 384 | . . 3 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
3 | 2 | rexbii 3070 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (¬ 𝜑 → 𝜓)) |
4 | df-or 384 | . . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | |
5 | ralnex 3021 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) | |
6 | 5 | imbi1i 338 | . . 3 ⊢ ((∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) ↔ (¬ ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
7 | 4, 6 | bitr4i 267 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) |
8 | 1, 3, 7 | 3bitr4i 292 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∨ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 382 ∀wral 2941 ∃wrex 2942 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-ex 1745 df-ral 2946 df-rex 2947 |
This theorem is referenced by: r19.44v 3123 r19.45v 3124 r19.45zv 4101 r19.44zv 4102 iunun 4636 wemapsolem 8496 pythagtriplem2 15569 pythagtrip 15586 dcubic 24618 legtrid 25531 axcontlem4 25892 erdszelem11 31309 soseq 31879 seglelin 32348 diophun 37654 rexzrexnn0 37685 ldepslinc 42623 |
Copyright terms: Public domain | W3C validator |