Metamath Proof Explorer

Theorem uniprg

Description: The union of a pair is the union of its members. Proposition 5.7 of TakeutiZaring p. 16. (Contributed by NM, 25-Aug-2006) Avoid using unipr to prove it from uniprg . (Revised by BJ, 1-Sep-2024)

Ref Expression
Assertion uniprg ⊢ A ∈ V ∧ B ∈ W → ⋃ A B = A ∪ B

Proof

Step Hyp Ref Expression
1 vex ⊢ y ∈ V
2 1 elpr ⊢ y ∈ A B ↔ y = A ∨ y = B
3 2 anbi2i ⊢ x ∈ y ∧ y ∈ A B ↔ x ∈ y ∧ y = A ∨ y = B
4 ancom ⊢ x ∈ y ∧ y = A ∨ y = B ↔ y = A ∨ y = B ∧ x ∈ y
5 andir ⊢ y = A ∨ y = B ∧ x ∈ y ↔ y = A ∧ x ∈ y ∨ y = B ∧ x ∈ y
6 4 5 bitri ⊢ x ∈ y ∧ y = A ∨ y = B ↔ y = A ∧ x ∈ y ∨ y = B ∧ x ∈ y
7 3 6 bitri ⊢ x ∈ y ∧ y ∈ A B ↔ y = A ∧ x ∈ y ∨ y = B ∧ x ∈ y
8 7 exbii ⊢ ∃ y x ∈ y ∧ y ∈ A B ↔ ∃ y y = A ∧ x ∈ y ∨ y = B ∧ x ∈ y
9 19.43 ⊢ ∃ y y = A ∧ x ∈ y ∨ y = B ∧ x ∈ y ↔ ∃ y y = A ∧ x ∈ y ∨ ∃ y y = B ∧ x ∈ y
10 8 9 bitri ⊢ ∃ y x ∈ y ∧ y ∈ A B ↔ ∃ y y = A ∧ x ∈ y ∨ ∃ y y = B ∧ x ∈ y
11 clel3g ⊢ A ∈ V → x ∈ A ↔ ∃ y y = A ∧ x ∈ y
12 11 bicomd ⊢ A ∈ V → ∃ y y = A ∧ x ∈ y ↔ x ∈ A
13 12 adantr ⊢ A ∈ V ∧ B ∈ W → ∃ y y = A ∧ x ∈ y ↔ x ∈ A
14 clel3g ⊢ B ∈ W → x ∈ B ↔ ∃ y y = B ∧ x ∈ y
15 14 bicomd ⊢ B ∈ W → ∃ y y = B ∧ x ∈ y ↔ x ∈ B
16 15 adantl ⊢ A ∈ V ∧ B ∈ W → ∃ y y = B ∧ x ∈ y ↔ x ∈ B
17 13 16 orbi12d ⊢ A ∈ V ∧ B ∈ W → ∃ y y = A ∧ x ∈ y ∨ ∃ y y = B ∧ x ∈ y ↔ x ∈ A ∨ x ∈ B
18 10 17 syl5bb ⊢ A ∈ V ∧ B ∈ W → ∃ y x ∈ y ∧ y ∈ A B ↔ x ∈ A ∨ x ∈ B
19 18 abbidv ⊢ A ∈ V ∧ B ∈ W → x | ∃ y x ∈ y ∧ y ∈ A B = x | x ∈ A ∨ x ∈ B
20 df-uni ⊢ ⋃ A B = x | ∃ y x ∈ y ∧ y ∈ A B
21 df-un ⊢ A ∪ B = x | x ∈ A ∨ x ∈ B
22 19 20 21 3eqtr4g ⊢ A ∈ V ∧ B ∈ W → ⋃ A B = A ∪ B