Proof 01. 1 ⊢ A ⊆ B, hypo. 02. 2 ⊢ x ∈ A ∪ B, hypo. 03. 2 ⊢ x ∈ A ∨ x ∈ B, union_elim 2. 04. 4 ⊢ x ∈ A, hypo. 05. 1, 4 ⊢ x ∈ B, incl_elim 1 4. 06. 6 ⊢ x ∈ B, hypo. 07. 1, 2 ⊢ x ∈ B, disj_elim 3 5 6. 08. 1 ⊢ x ∈ A ∪ B → x ∈ B, subj_intro 7. 09. 1 ⊢ ∀x. x ∈ A ∪ B → x ∈ B, uq_intro 8. 10. 1 ⊢ A ∪ B ⊆ B, incl_intro 9. 11. ⊢ B ⊆ A ∪ B, union_incl_right. 12. 1 ⊢ A ∪ B = B, incl_antisym 10 11. union_from_incl. ⊢ A ⊆ B → A ∪ B = B, subj_intro 12.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.