| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rexun | Structured version Visualization version GIF version | ||
| Description: Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.) |
| Ref | Expression |
|---|---|
| rexun | ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑)) | |
| 2 | 19.43 1882 | . . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∨ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))) | |
| 3 | elun 4153 | . . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) | |
| 4 | 3 | anbi1i 624 | . . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝜑)) |
| 5 | andir 1011 | . . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑))) | |
| 6 | 4, 5 | bitri 275 | . . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑))) |
| 7 | 6 | exbii 1848 | . . 3 ⊢ (∃𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑))) |
| 8 | df-rex 3071 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 9 | df-rex 3071 | . . . 4 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)) | |
| 10 | 8, 9 | orbi12i 915 | . . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∨ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))) |
| 11 | 2, 7, 10 | 3bitr4i 303 | . 2 ⊢ (∃𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑)) |
| 12 | 1, 11 | bitri 275 | 1 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∨ wo 848 ∃wex 1779 ∈ wcel 2108 ∃wrex 3070 ∪ cun 3949 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rex 3071 df-v 3482 df-un 3956 |
| This theorem is referenced by: rexprgf 4695 rextpg 4699 iunxun 5094 unima 6984 oarec 8600 naddunif 8731 zornn0g 10545 scshwfzeqfzo 14865 rpnnen2lem12 16261 dvdsprmpweqnn 16923 vdwlem6 17024 pmatcollpw3fi1 22794 cmpfi 23416 sleadd1 28022 addsasslem1 28036 addsasslem2 28037 addsdilem1 28177 addsdilem2 28178 mulsasslem1 28189 mulsasslem2 28190 elntg2 29000 rprmdvdsprod 33562 satfvsucsuc 35370 poimirlem25 37652 |
| Copyright terms: Public domain | W3C validator |