Theorem rexun

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

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

Proof

Step	Hyp	Ref	Expression
1		df-rex	⊢ ( ∃ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) )
2		19.43	⊢ ( ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
3		elun	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
4	3	anbi1i	⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ 𝜑 ) )
5		andir	⊢ ( ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
6	4 5	bitri	⊢ ( ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
7	6	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
8		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
9		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐵 𝜑 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
10	8 9	orbi12i	⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐵 𝜑 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
11	2 7 10	3bitr4i	⊢ ( ∃ 𝑥 ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝜑 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐵 𝜑 ) )
12	1 11	bitri	⊢ ( ∃ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐵 𝜑 ) )