Proof 01. 1 ⊢ A ∪ B = B, hypo. 02. 2 ⊢ x ∈ A, hypo. 03. 2 ⊢ x ∈ A ∪ B, union_introl 2. 04. 1, 2 ⊢ x ∈ B, eq_subst 1 3, P u ↔ x ∈ u. 05. 1 ⊢ x ∈ A → x ∈ B, subj_intro 4. 06. 1 ⊢ ∀x. x ∈ A → x ∈ B, uq_intro 5. 07. 1 ⊢ A ⊆ B, incl_intro 6. incl_from_union. ⊢ A ∪ B = B → A ⊆ B, subj_intro 7.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.