Theorem rexun 4137

Description: Restricted existential quantification over union. (Contributed by Jeff Madsen, 5-Jan-2011.)

Assertion

Ref	Expression
rexun	⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑))

Proof of Theorem rexun

Step	Hyp	Ref	Expression
1		df-rex 3063	. 2 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑))
2		19.43 1884	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∨ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
3		elun 4094	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	anbi1i 625	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝜑))
5		andir 1011	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑)))
6	4, 5	bitri 275	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑)))
7	6	exbii 1850	. . 3 ⊢ (∃𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑)))
8		df-rex 3063	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9		df-rex 3063	. . . 4 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
10	8, 9	orbi12i 915	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∨ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
11	2, 7, 10	3bitr4i 303	. 2 ⊢ (∃𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑))
12	1, 11	bitri 275	1 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 848  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3432  df-un 3895

This theorem is referenced by:  rexprgf  4640  rextpg  4644  iunxun  5037  unima  6909  oarec  8490  naddunif  8622  zornn0g  10418  scshwfzeqfzo  14779  rpnnen2lem12  16183  dvdsprmpweqnn  16847  vdwlem6  16948  pmatcollpw3fi1  22763  cmpfi  23383  leadds1  27995  addsasslem1  28009  addsasslem2  28010  addsdilem1  28157  addsdilem2  28158  mulsasslem1  28169  mulsasslem2  28170  elntg2  29068  domnprodeq0  33352  rprmdvdsprod  33609  satfvsucsuc  35563  poimirlem25  37980