Proof 01. 1 ⊢ A ⊆ X, hypo. 02. 2 ⊢ x ∈ X \ (X \ A), hypo. 03. 2 ⊢ x ∈ X, diff_eliml 2. 04. 2 ⊢ ¬x ∈ X \ A, diff_elimr 2. 05. 5 ⊢ ¬x ∈ A, hypo. 06. 2, 5 ⊢ x ∈ X \ A, diff_intro 3 5. 07. 2, 5 ⊢ ⊥, neg_elim 4 6. 08. 2 ⊢ ¬¬x ∈ A, neg_intro 7. 09. 2 ⊢ x ∈ A, dne 8. 10. ⊢ x ∈ X \ (X \ A) → x ∈ A, subj_intro 9. 11. 11 ⊢ x ∈ A, hypo. 12. 1, 11 ⊢ x ∈ X, incl_elim 1 11. 13. 13 ⊢ x ∈ X \ A, hypo. 14. 13 ⊢ ¬x ∈ A, diff_elimr 13. 15. 11, 13 ⊢ ⊥, neg_elim 14 11. 16. 11 ⊢ ¬x ∈ X \ A, neg_intro 15. 17. 1, 11 ⊢ x ∈ X \ (X \ A), diff_intro 12 16. 18. 1 ⊢ x ∈ A → x ∈ X \ (X \ A), subj_intro 17. 19. 1 ⊢ x ∈ X \ (X \ A) ↔ x ∈ A, bij_intro 10 18. 20. 1 ⊢ ∀x. x ∈ X \ (X \ A) ↔ x ∈ A, uq_intro 19. 21. 1 ⊢ X \ (X \ A) = A, ext 20. diff_is_involution. ⊢ A ⊆ X → X \ (X \ A) = A, subj_intro 21.
Dependencies
The given proof depends on six axioms:
comp, efq, eq_refl, eq_subst, ext, lem.