Metamath Proof Explorer


Table of Contents - 21.20.5.10. Russell's paradox

A few results around Russell's paradox. For clarity, we prove separately a FOL statement (now in the main part as ru0) and then two versions (bj-ru1 and bj-ru). Special attention is put on minimizing axiom depencencies.

  1. bj-ru1
  2. bj-ru