Theorem empty_diff

Proof
01. 1 ⊢ A \ B = ∅, hypo.
02. 2 ⊢ x ∈ A, hypo.
03. 3 ⊢ ¬x ∈ B, hypo.
04. 2, 3 ⊢ x ∈ A \ B, diff_intro 2 3.
05. 1, 2, 3 ⊢ x ∈ ∅, eq_subst 1 4, P u ↔ x ∈ u.
06. 1, 2, 3 ⊢ ⊥, empty_contra 5.
07. 1, 2 ⊢ ¬¬x ∈ B, neg_intro 6.
08. 1, 2 ⊢ x ∈ B, dne 7.
09. 1 ⊢ x ∈ A → x ∈ B, subj_intro 8.
10. 1 ⊢ ∀x. x ∈ A → x ∈ B, uq_intro 9.
11. 1 ⊢ A ⊆ B, incl_intro 10.
empty_diff. ⊢ A \ B = ∅ → A ⊆ B, subj_intro 11.

Dependencies
The given proof depends on five axioms:
comp, efq, eq_refl, eq_subst, lem.