Metamath Proof Explorer

Theorem bj-unexg

Description: Existence of binary unions of sets, proved from ax-bj-bun . (Contributed by BJ, 12-Jan-2025) (Proof modification is discouraged.)

Ref Expression
Assertion bj-unexg ⊢ A ∈ V ∧ B ∈ W → A ∪ B ∈ V

Proof

Step Hyp Ref Expression
1 elissetv ⊢ A ∈ V → ∃ x x = A
2 elissetv ⊢ B ∈ W → ∃ y y = B
3 exdistrv ⊢ ∃ x ∃ y x = A ∧ y = B ↔ ∃ x x = A ∧ ∃ y y = B
4 uneq12 ⊢ x = A ∧ y = B → x ∪ y = A ∪ B
5 ax-bj-bun ⊢ ∀ x ∀ y ∃ z ∀ t t ∈ z ↔ t ∈ x ∨ t ∈ y
6 5 spi ⊢ ∀ y ∃ z ∀ t t ∈ z ↔ t ∈ x ∨ t ∈ y
7 6 spi ⊢ ∃ z ∀ t t ∈ z ↔ t ∈ x ∨ t ∈ y
8 bj-axbun ⊢ x ∪ y ∈ V ↔ ∃ z ∀ t t ∈ z ↔ t ∈ x ∨ t ∈ y
9 7 8 mpbir ⊢ x ∪ y ∈ V
10 4 9 eqeltrrdi ⊢ x = A ∧ y = B → A ∪ B ∈ V
11 10 exlimiv ⊢ ∃ y x = A ∧ y = B → A ∪ B ∈ V
12 11 exlimiv ⊢ ∃ x ∃ y x = A ∧ y = B → A ∪ B ∈ V
13 3 12 sylbir ⊢ ∃ x x = A ∧ ∃ y y = B → A ∪ B ∈ V
14 1 2 13 syl2an ⊢ A ∈ V ∧ B ∈ W → A ∪ B ∈ V