Proof 01. 1 ⊢ A1 ⊆ B, hypo. 02. 2 ⊢ A2 ⊆ B, hypo. 03. 1, 2 ⊢ A1 ∪ A2 ⊆ B ∪ B, union_incl_in_union 1 2. 04. ⊢ B ∪ B = B, union_idem. 05. 1, 2 ⊢ A1 ∪ A2 ⊆ B, eq_subst 4 3, P u ↔ A1 ∪ A2 ⊆ u. union_incl_in. ⊢ A1 ⊆ B → A2 ⊆ B → A1 ∪ A2 ⊆ B, subj_intro_ii 5.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.