Minor shortenings, moving, cleaning (#4603)

* Shorten snexg and bj-abex. Typos. * Move two theorems out of Section 'Theorems requiring empty set existence' when they do not require it. Add cross-links and clarify comments.
metamath · Jan 25, 2025 · 8dad40a · 8dad40a
1 parent fec5d89
commit 8dad40a
Show file tree

Hide file tree

Showing 2 changed files with 67 additions and 46 deletions.
diff --git a/discouraged b/discouraged
@@ -19854,7 +19854,7 @@ Proof modification of "bj-19.21t0" is discouraged (39 steps).
 Proof modification of "bj-19.41al" is discouraged (51 steps).
 Proof modification of "bj-a1k" is discouraged (10 steps).
 Proof modification of "bj-ab0" is discouraged (39 steps).
-Proof modification of "bj-abex" is discouraged (35 steps).
+Proof modification of "bj-abex" is discouraged (32 steps).
 Proof modification of "bj-abf" is discouraged (13 steps).
 Proof modification of "bj-ablsscmn" is discouraged (10 steps).
 Proof modification of "bj-ablsscmnel" is discouraged (5 steps).