elnanel revised

avekens · Nov 18, 2023 · 149f892 · 149f892
1 parent 39d984c
commit 149f892
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/discouraged b/discouraged
@@ -5649,6 +5649,7 @@
 "ellnop" is used by "lnopl".
 "ellnop" is used by "lnopmi".
 "ellnop" is used by "unoplin".
+"elnanel" is used by "elnanelprv".
 "elni" is used by "0npi".
 "elni" is used by "1pi".
 "elni" is used by "addclpi".
@@ -15075,6 +15076,7 @@ New usage of "elimphu" is discouraged (3 uses).
 New usage of "elissetOLD" is discouraged (0 uses).
 New usage of "ellnfn" is discouraged (5 uses).
 New usage of "ellnop" is discouraged (9 uses).
+New usage of "elnanel" is discouraged (1 uses).
 New usage of "elni" is discouraged (7 uses).
 New usage of "elni2" is discouraged (7 uses).
 New usage of "elnlfn" is discouraged (4 uses).

diff --git a/set.mm b/set.mm
@@ -91095,8 +91095,10 @@ is that it denies the existence of a set containing itself ( ~ elirrv ).
     ( cvv wcel wa wn cep wfr zfregfr efrn2lp mpan elex anim12i con3i pm2.61i )
     ACDZBCDZEZABDZBADZEZFZCGHRUBCICABJKUARSPTQABLBALMNO $.
 
-  $( Two classes are not elements of each other simultaneously.  (Contributed
-     by AV, 5-Nov-2023.) $)
+  $( Two classes are not elements of each other simultaneously.  This is just a
+     rewriting of ~ en2lp and serves as an example in the context of Godel
+     codes, see ~ elnanelprv .  (Contributed by AV, 5-Nov-2023.)
+     (New usage is discouraged.) $)
   elnanel $p |- ( A e. B -/\ B e. A ) $=
     ( wcel wnan wa wn en2lp df-nan mpbir ) ABCZBACZDJKEFABGJKHI $.