Metamath Proof Explorer

Theorem unipr

Description: The union of a pair is the union of its members. Proposition 5.7 of TakeutiZaring p. 16. (Contributed by NM, 23-Aug-1993)

Ref Expression
Hypotheses unipr.1 ⊢ A ∈ V
unipr.2 ⊢ B ∈ V
Assertion unipr ⊢ ⋃ A B = A ∪ B

Proof

Step Hyp Ref Expression
1 unipr.1 ⊢ A ∈ V
2 unipr.2 ⊢ B ∈ V
3 19.43 ⊢ ∃ y x ∈ y ∧ y = A ∨ x ∈ y ∧ y = B ↔ ∃ y x ∈ y ∧ y = A ∨ ∃ y x ∈ y ∧ y = B
4 vex ⊢ y ∈ V
5 4 elpr ⊢ y ∈ A B ↔ y = A ∨ y = B
6 5 anbi2i ⊢ x ∈ y ∧ y ∈ A B ↔ x ∈ y ∧ y = A ∨ y = B
7 andi ⊢ x ∈ y ∧ y = A ∨ y = B ↔ x ∈ y ∧ y = A ∨ x ∈ y ∧ y = B
8 6 7 bitri ⊢ x ∈ y ∧ y ∈ A B ↔ x ∈ y ∧ y = A ∨ x ∈ y ∧ y = B
9 8 exbii ⊢ ∃ y x ∈ y ∧ y ∈ A B ↔ ∃ y x ∈ y ∧ y = A ∨ x ∈ y ∧ y = B
10 1 clel3 ⊢ x ∈ A ↔ ∃ y y = A ∧ x ∈ y
11 exancom ⊢ ∃ y y = A ∧ x ∈ y ↔ ∃ y x ∈ y ∧ y = A
12 10 11 bitri ⊢ x ∈ A ↔ ∃ y x ∈ y ∧ y = A
13 2 clel3 ⊢ x ∈ B ↔ ∃ y y = B ∧ x ∈ y
14 exancom ⊢ ∃ y y = B ∧ x ∈ y ↔ ∃ y x ∈ y ∧ y = B
15 13 14 bitri ⊢ x ∈ B ↔ ∃ y x ∈ y ∧ y = B
16 12 15 orbi12i ⊢ x ∈ A ∨ x ∈ B ↔ ∃ y x ∈ y ∧ y = A ∨ ∃ y x ∈ y ∧ y = B
17 3 9 16 3bitr4ri ⊢ x ∈ A ∨ x ∈ B ↔ ∃ y x ∈ y ∧ y ∈ A B
18 17 abbii ⊢ x | x ∈ A ∨ x ∈ B = x | ∃ y x ∈ y ∧ y ∈ A B
19 df-un ⊢ A ∪ B = x | x ∈ A ∨ x ∈ B
20 df-uni ⊢ ⋃ A B = x | ∃ y x ∈ y ∧ y ∈ A B
21 18 19 20 3eqtr4ri ⊢ ⋃ A B = A ∪ B