Theorem union_introl

Proof
01. 1 ⊢ x ∈ A, hypo.
02. 1 ⊢ x ∈ A ∨ x ∈ B, disj_introl 1.
03. 1 ⊢ x ∈ A ∪ B, union_intro 2.
union_introl. ⊢ x ∈ A → x ∈ A ∪ B, subj_intro 3.

Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.