Proof 01. 1 ⊢ A ⊆ X, hypo. 02. 1 ⊢ A ∪ X = X, union_from_incl 1. 03. ⊢ X ∪ A = A ∪ X, union_comm. 04. 1 ⊢ X ∪ A = X, eq_trans 3 2. 05. ⊢ (X \ A) ∪ A = X ∪ A, diff_union. 06. 1 ⊢ (X \ A) ∪ A = X, eq_trans 5 4. diff_union_subclass. ⊢ A ⊆ X → (X \ A) ∪ A = X, subj_intro 6.
Dependencies
The given proof depends on five axioms:
comp, eq_refl, eq_subst, ext, lem.