Add $j usage (#3251)

This is intended to be an automatically enforced restriction on what
statements can be used in a proof.  Document it in j-commands.html.
Add a number of examples in iset.mm and set.mm.

Author: jkingdon

iset.mm

@@ -24988,6 +24988,7 @@ with a weaker Subset (or Separation) Axiom asserting that ` A ` is a set
       AEZFDUKFGZHULBCZUKIZBJUNBUNABKZUJQZALZUQBBKZURHZQZURMUPUTABUIUMIZUOURUJUS
       UIUMUMNUJAAKZHVAUSUIUIOVAVBURVAUIUMUIUMVARZVCPSUAUBUCUDUJAUMUETUFBUKUGTUK
       FOUH $.
+    $( $j usage 'ru' avoids 'ax-setind'; $)
   $}
 
 

mm-j-commands.html

@@ -97,6 +97,14 @@ <h2>Syntax and definitions</h2>
 though it makes use of a theorem that depends on <code>A, C</code> which
 cannot be minimized in this way.</p>
 
+<code>$j usage 'THEOREM' avoids 'STATEMENT' ...;</code>
+
+<p>The proof of THEOREM should not use any listed STATEMENT,
+directly or indirectly.  Although STATEMENT will often be an axiom
+(for example the axiom of choice or the axiom of infinity), it can
+also be a theorem which this proof should avoid.  Tools are encouraged
+to check for violations and flag them as errors.</p>
+
 <code>$j type_conversions;</code>
 
 <p>Adds all "type conversions" to the grammatical parser. These are