Metamath Proof Explorer

Theorem mptun

Description: Union of mappings which are mutually compatible. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion mptun ⊢ x ∈ A ∪ B ⟼ C = x ∈ A ⟼ C ∪ x ∈ B ⟼ C

Proof

Step Hyp Ref Expression
1 df-mpt ⊢ x ∈ A ∪ B ⟼ C = x y | x ∈ A ∪ B ∧ y = C
2 df-mpt ⊢ x ∈ A ⟼ C = x y | x ∈ A ∧ y = C
3 df-mpt ⊢ x ∈ B ⟼ C = x y | x ∈ B ∧ y = C
4 2 3 uneq12i ⊢ x ∈ A ⟼ C ∪ x ∈ B ⟼ C = x y | x ∈ A ∧ y = C ∪ x y | x ∈ B ∧ y = C
5 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
6 5 anbi1i ⊢ x ∈ A ∪ B ∧ y = C ↔ x ∈ A ∨ x ∈ B ∧ y = C
7 andir ⊢ x ∈ A ∨ x ∈ B ∧ y = C ↔ x ∈ A ∧ y = C ∨ x ∈ B ∧ y = C
8 6 7 bitri ⊢ x ∈ A ∪ B ∧ y = C ↔ x ∈ A ∧ y = C ∨ x ∈ B ∧ y = C
9 8 opabbii ⊢ x y | x ∈ A ∪ B ∧ y = C = x y | x ∈ A ∧ y = C ∨ x ∈ B ∧ y = C
10 unopab ⊢ x y | x ∈ A ∧ y = C ∪ x y | x ∈ B ∧ y = C = x y | x ∈ A ∧ y = C ∨ x ∈ B ∧ y = C
11 9 10 eqtr4i ⊢ x y | x ∈ A ∪ B ∧ y = C = x y | x ∈ A ∧ y = C ∪ x y | x ∈ B ∧ y = C
12 4 11 eqtr4i ⊢ x ∈ A ⟼ C ∪ x ∈ B ⟼ C = x y | x ∈ A ∪ B ∧ y = C
13 1 12 eqtr4i ⊢ x ∈ A ∪ B ⟼ C = x ∈ A ⟼ C ∪ x ∈ B ⟼ C