Proof 01. 1 ⊢ x ∈ B, hypo. 02. 1 ⊢ x ∈ A ∪ B, union_intror 1. 03. ⊢ x ∈ B → x ∈ A ∪ B, subj_intro 2. 04. ⊢ ∀x. x ∈ B → x ∈ A ∪ B, uq_intro 3. union_incl_right. ⊢ B ⊆ A ∪ B, incl_intro 4.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.