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

Metamath Proof Explorer

Theorem rabun2

Description: Abstraction restricted to a union. (Contributed by Stefan O'Rear, 5-Feb-2015)

Ref Expression
Assertion rabun2 ⊢ x ∈ A ∪ B | φ = x ∈ A | φ ∪ x ∈ B | φ

Proof

Step Hyp Ref Expression
1 df-rab ⊢ x ∈ A ∪ B | φ = x | x ∈ A ∪ B ∧ φ
2 df-rab ⊢ x ∈ A | φ = x | x ∈ A ∧ φ
3 df-rab ⊢ x ∈ B | φ = x | x ∈ B ∧ φ
4 2 3 uneq12i ⊢ x ∈ A | φ ∪ x ∈ B | φ = x | x ∈ A ∧ φ ∪ x | x ∈ B ∧ φ
5 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
6 5 anbi1i ⊢ x ∈ A ∪ B ∧ φ ↔ x ∈ A ∨ x ∈ B ∧ φ
7 andir ⊢ x ∈ A ∨ x ∈ B ∧ φ ↔ x ∈ A ∧ φ ∨ x ∈ B ∧ φ
8 6 7 bitri ⊢ x ∈ A ∪ B ∧ φ ↔ x ∈ A ∧ φ ∨ x ∈ B ∧ φ
9 8 abbii ⊢ x | x ∈ A ∪ B ∧ φ = x | x ∈ A ∧ φ ∨ x ∈ B ∧ φ
10 unab ⊢ x | x ∈ A ∧ φ ∪ x | x ∈ B ∧ φ = x | x ∈ A ∧ φ ∨ x ∈ B ∧ φ
11 9 10 eqtr4i ⊢ x | x ∈ A ∪ B ∧ φ = x | x ∈ A ∧ φ ∪ x | x ∈ B ∧ φ
12 4 11 eqtr4i ⊢ x ∈ A | φ ∪ x ∈ B | φ = x | x ∈ A ∪ B ∧ φ
13 1 12 eqtr4i ⊢ x ∈ A ∪ B | φ = x ∈ A | φ ∪ x ∈ B | φ