This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ∃ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∨ ∃ 𝑥 ∈ 𝐵 𝜑 ) )