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