Proof
01. 1 ⊢ set x ∧ set y, hypo.
02. 1 ⊢ set x, conj_eliml 1.
03. 1 ⊢ set y, conj_elimr 1.
04. 4 ⊢ u ∈ ⋃{x, y}, hypo.
05. 4 ⊢ ∃a. a ∈ {x, y} ∧ u ∈ a, Union_elim 4.
06. 6 ⊢ a ∈ {x, y} ∧ u ∈ a, hypo.
07. 6 ⊢ a ∈ {x, y}, conj_eliml 6.
08. 6 ⊢ u ∈ a, conj_elimr 6.
09. 6 ⊢ a ∈ {x} ∨ a ∈ {y}, union_elim 7.
10. 10 ⊢ a ∈ {x}, hypo.
11. 1, 10 ⊢ a = x, sg_elim 2 10.
12. 1, 6, 10 ⊢ u ∈ x, eq_subst 11 8, P x ↔ u ∈ x.
13. 1, 6, 10 ⊢ u ∈ x ∪ y, union_introl 12.
14. 14 ⊢ a ∈ {y}, hypo.
15. 1, 14 ⊢ a = y, sg_elim 3 14.
16. 1, 6, 14 ⊢ u ∈ y, eq_subst 15 8, P x ↔ u ∈ x.
17. 1, 6, 14 ⊢ u ∈ x ∪ y, union_intror 16.
18. 1, 6 ⊢ u ∈ x ∪ y, disj_elim 9 13 17.
19. 1, 4 ⊢ u ∈ x ∪ y, ex_elim 5 18.
20. 1 ⊢ u ∈ ⋃{x, y} → u ∈ x ∪ y, subj_intro 19.
21. 1 ⊢ ∀u. u ∈ ⋃{x, y} → u ∈ x ∪ y, uq_intro 20.
22. 1 ⊢ ⋃{x, y} ⊆ x ∪ y, incl_intro 21.
23. 23 ⊢ u ∈ x ∪ y, hypo.
24. 23 ⊢ u ∈ x ∨ u ∈ y, union_elim 23.
25. 25 ⊢ u ∈ x, hypo.
26. 1 ⊢ x ∈ {x, y}, in21 2.
27. 1, 25 ⊢ x ∈ {x, y} ∧ u ∈ x, conj_intro 26 25.
28. 1, 25 ⊢ ∃a. a ∈ {x, y} ∧ u ∈ a, ex_intro 27.
29. 1, 25 ⊢ u ∈ ⋃{x, y}, Union_intro_ex 28.
30. 30 ⊢ u ∈ y, hypo.
31. 1 ⊢ y ∈ {x, y}, in22 3.
32. 1, 30 ⊢ y ∈ {x, y} ∧ u ∈ y, conj_intro 31 30.
33. 1, 30 ⊢ ∃a. a ∈ {x, y} ∧ u ∈ a, ex_intro 32.
34. 1, 30 ⊢ u ∈ ⋃{x, y}, Union_intro_ex 33.
35. 1, 23 ⊢ u ∈ ⋃{x, y}, disj_elim 24 29 34.
36. 1 ⊢ u ∈ x ∪ y → u ∈ ⋃{x, y}, subj_intro 35.
37. 1 ⊢ ∀u. u ∈ x ∪ y → u ∈ ⋃{x, y}, uq_intro 36.
38. 1 ⊢ x ∪ y ⊆ ⋃{x, y}, incl_intro 37.
39. 1 ⊢ ⋃{x, y} = x ∪ y, incl_antisym 22 38.
Union_pair_set. ⊢ set x ∧ set y → ⋃{x, y} = x ∪ y, subj_intro 39.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.