Proof 01. 1 ⊢ A ⊆ B, hypo. 02. 2 ⊢ x ∈ ⋃A, hypo. 03. 2 ⊢ ∃y. y ∈ A ∧ x ∈ y, Union_elim 2. 04. 4 ⊢ y ∈ A ∧ x ∈ y, hypo. 05. 4 ⊢ y ∈ A, conj_eliml 4. 06. 4 ⊢ x ∈ y, conj_elimr 4. 07. 1, 4 ⊢ y ∈ B, incl_elim 1 5. 08. 1, 4 ⊢ y ∈ B ∧ x ∈ y, conj_intro 7 6. 09. 1, 4 ⊢ ∃y. y ∈ B ∧ x ∈ y, ex_intro 8. 10. 1, 4 ⊢ x ∈ ⋃B, Union_intro_ex 9. 11. 1, 2 ⊢ x ∈ ⋃B, ex_elim 3 10. 12. 1 ⊢ x ∈ ⋃A → x ∈ ⋃B, subj_intro 11. 13. 1 ⊢ ∀x. x ∈ ⋃A → x ∈ ⋃B, uq_intro 12. 14. 1 ⊢ ⋃A ⊆ ⋃B, incl_intro 13. Union_inc. ⊢ A ⊆ B → ⋃A ⊆ ⋃B, subj_intro 14.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.