Metamath Proof Explorer

Table of Contents - 21.20.5.9. Restricted nonfreeness

In this subsection, we define restricted nonfreeness (or relative nonfreeness).

1. wrnf
2. df-bj-rnf