Proof
01. 1 ⊢ R = {x | ¬x ∈ x}, hypo.
02. 2 ⊢ u ∈ R, hypo.
03. 1, 2 ⊢ u ∈ {x | ¬x ∈ x}, eq_subst 1 2.
04. 1, 2 ⊢ ¬u ∈ u, comp_elim 3.
05. 1 ⊢ u ∈ R → ¬u ∈ u, subj_intro 4.
06. 1 ⊢ R ∈ R → ¬R ∈ R, 5.
07. 7 ⊢ set R, hypo.
08. 8 ⊢ ¬R ∈ R, hypo.
09. 7, 8 ⊢ R ∈ {x | ¬x ∈ x}, comp_intro 7 8.
10. 1, 7, 8 ⊢ R ∈ R, eq_subst_rev 1 9, P x ↔ R ∈ x.
11. 1, 7 ⊢ ¬R ∈ R → R ∈ R, subj_intro 10.
12. 1, 7 ⊢ R ∈ R ↔ ¬R ∈ R, bij_intro 6 11.
13. ⊢ (R ∈ R ↔ ¬R ∈ R) → ⊥, diag_contra.
14. 1, 7 ⊢ ⊥, subj_elim 13 12.
15. 1 ⊢ ¬set R, neg_intro 14.
16. ⊢ R = {x | ¬x ∈ x} → ¬set R, subj_intro 15.
17. ⊢ DiagCl = {x | ¬x ∈ x} → ¬set DiagCl, 16.
DiagCl_is_proper. ⊢ ¬set DiagCl, subj_elim 17 DiagCl_eq.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.