Theorem rexun 4146

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 3057	. 2 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∃𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑))
2		19.43 1883	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∨ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
3		elun 4103	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	anbi1i 624	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝜑))
5		andir 1010	. . . . 5 ⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑)))
6	4, 5	bitri 275	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑)))
7	6	exbii 1849	. . 3 ⊢ (∃𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∨ (𝑥 ∈ 𝐵 ∧ 𝜑)))
8		df-rex 3057	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
9		df-rex 3057	. . . 4 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
10	8, 9	orbi12i 914	. . 3 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∨ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
11	2, 7, 10	3bitr4i 303	. 2 ⊢ (∃𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑))
12	1, 11	bitri 275	1 ⊢ (∃𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056   ∪ cun 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-v 3438  df-un 3907

This theorem is referenced by:  rexprgf  4648  rextpg  4652  iunxun  5042  unima  6897  oarec  8477  naddunif  8608  zornn0g  10393  scshwfzeqfzo  14730  rpnnen2lem12  16131  dvdsprmpweqnn  16794  vdwlem6  16895  pmatcollpw3fi1  22701  cmpfi  23321  sleadd1  27930  addsasslem1  27944  addsasslem2  27945  addsdilem1  28088  addsdilem2  28089  mulsasslem1  28100  mulsasslem2  28101  elntg2  28961  rprmdvdsprod  33494  satfvsucsuc  35397  poimirlem25  37684