incl_contraposition

Theorem incl_contraposition

Theorem. incl_contraposition
A ⊆ B → X \ B ⊆ X \ A

Proof
01. 1 ⊢ A ⊆ B, hypo.
02. 2 ⊢ x ∈ X \ B, hypo.
03. 2 ⊢ x ∈ X, diff_eliml 2.
04. 2 ⊢ ¬x ∈ B, diff_elimr 2.
05. 1 ⊢ x ∈ A → x ∈ B, incl_elim 1.
06. 1 ⊢ ¬x ∈ B → ¬x ∈ A, contraposition 5.
07. 1, 2 ⊢ ¬x ∈ A, subj_elim 6 4.
08. 1, 2 ⊢ x ∈ X \ A, diff_intro 3 7.
09. 1 ⊢ x ∈ X \ B → x ∈ X \ A, subj_intro 8.
10. 1 ⊢ ∀x. x ∈ X \ B → x ∈ X \ A, uq_intro 9.
11. 1 ⊢ X \ B ⊆ X \ A, incl_intro 10.
incl_contraposition. ⊢ A ⊆ B → X \ B ⊆ X \ A,
  subj_intro 11.

Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.