update comments of other restricted quantifiers. (#3266)

* delete outdated OLD theorems

* discouraged

* add a note to df-rex

* update comment of df-rmo

* improve the comment of df-rab

* typos

* rewrap

* style

* typo

* typo

* typo

Author: wlammen

discouraged

@@ -13293,10 +13293,6 @@ New usage of "2uasban" is discouraged (0 uses).
 New usage of "2uasbanh" is discouraged (1 uses).
 New usage of "2uasbanhVD" is discouraged (0 uses).
 New usage of "2zrngALT" is discouraged (0 uses).
-New usage of "3adant2lOLD" is discouraged (0 uses).
-New usage of "3adant2rOLD" is discouraged (0 uses).
-New usage of "3adant3lOLD" is discouraged (0 uses).
-New usage of "3adant3rOLD" is discouraged (0 uses).
 New usage of "3anidm12p1" is discouraged (0 uses).
 New usage of "3anidm12p2" is discouraged (0 uses).
 New usage of "3atnelvolN" is discouraged (2 uses).
@@ -18100,10 +18096,6 @@ Proof modification of "2uasbanh" is discouraged (214 steps).
 Proof modification of "2uasbanhVD" is discouraged (313 steps).
 Proof modification of "2zrngALT" is discouraged (207 steps).
 Proof modification of "31prm" is discouraged (541 steps).
-Proof modification of "3adant2lOLD" is discouraged (19 steps).
-Proof modification of "3adant2rOLD" is discouraged (19 steps).
-Proof modification of "3adant3lOLD" is discouraged (19 steps).
-Proof modification of "3adant3rOLD" is discouraged (19 steps).
 Proof modification of "3anidm12p1" is discouraged (5 steps).
 Proof modification of "3anidm12p2" is discouraged (19 steps).
 Proof modification of "3cnOLD" is discouraged (3 steps).

set.mm

@@ -9439,45 +9439,21 @@ This definition (in the form of ~ dfifp2 ) appears in Section II.24 of
     3adant2l $p |- ( ( ph /\ ( ta /\ ps ) /\ ch ) -> th ) $=
       ( wa simpr syl3an2 ) EBGABCDEBHFI $.
 
-    $( Obsolete version of ~ 3adant2l as of 25-Jun-2022.  (Contributed by NM,
-       8-Jan-2006.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    3adant2lOLD $p |- ( ( ph /\ ( ta /\ ps ) /\ ch ) -> th ) $=
-      ( wa 3com12 3adant1l ) EBGACDBACDEABCDFHIH $.
-
     $( Deduction adding a conjunct to antecedent.  (Contributed by NM,
        8-Jan-2006.)  (Proof shortened by Wolf Lammen, 25-Jun-2022.) $)
     3adant2r $p |- ( ( ph /\ ( ps /\ ta ) /\ ch ) -> th ) $=
       ( wa simpl syl3an2 ) BEGABCDBEHFI $.
 
-    $( Obsolete version of ~ 3adant2r as of 25-Jun-2022.  (Contributed by NM,
-       8-Jan-2006.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    3adant2rOLD $p |- ( ( ph /\ ( ps /\ ta ) /\ ch ) -> th ) $=
-      ( wa 3com12 3adant1r ) BEGACDBACDEABCDFHIH $.
-
     $( Deduction adding a conjunct to antecedent.  (Contributed by NM,
        8-Jan-2006.)  (Proof shortened by Wolf Lammen, 25-Jun-2022.) $)
     3adant3l $p |- ( ( ph /\ ps /\ ( ta /\ ch ) ) -> th ) $=
       ( wa simpr syl3an3 ) ECGABCDECHFI $.
 
-    $( Obsolete version of ~ 3adant3l as of 25-Jun-2022.  (Contributed by NM,
-       8-Jan-2006.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    3adant3lOLD $p |- ( ( ph /\ ps /\ ( ta /\ ch ) ) -> th ) $=
-      ( wa 3com13 3adant1l ) ECGBADCBADEABCDFHIH $.
-
     $( Deduction adding a conjunct to antecedent.  (Contributed by NM,
        8-Jan-2006.)  (Proof shortened by Wolf Lammen, 25-Jun-2022.) $)
     3adant3r $p |- ( ( ph /\ ps /\ ( ch /\ ta ) ) -> th ) $=
       ( wa simpl syl3an3 ) CEGABCDCEHFI $.
 
-    $( Obsolete version of ~ 3adant3r as of 25-Jun-2022.  (Contributed by NM,
-       8-Jan-2006.)  (Proof modification is discouraged.)
-       (New usage is discouraged.) $)
-    3adant3rOLD $p |- ( ( ph /\ ps /\ ( ch /\ ta ) ) -> th ) $=
-      ( wa 3com13 3adant1r ) CEGBADCBADEABCDFHIH $.
-
     $( Deduction adding a conjunct to antecedent.  (Contributed by NM,
        16-Feb-2008.) $)
     3adant3r1 $p |- ( ( ph /\ ( ta /\ ps /\ ch ) ) -> th ) $=
@@ -26956,19 +26932,57 @@ choice between (what we call) a "definitional form" where the shorter
   df-ral $a |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) ) $.
 
   $( Define restricted existential quantification.  Special case of Definition
-     4.15(4) of [TakeutiZaring] p. 22.  (Contributed by NM, 30-Aug-1993.) $)
+     4.15(4) of [TakeutiZaring] p. 22.
+
+     Note:  This notation is most often used to express that ` ph ` holds for
+     at least one element of a given class ` A ` .  For this reading
+     ` F/_ x A ` is required, though, for example, asserted when ` x ` and
+     ` A ` are disjoint.
+
+     Should instead ` A ` depend on ` x ` , you rather assert at least one
+     ` x ` fulfilling ` ph ` happens to be contained in the corresponding
+     ` A ( x ) ` .  This interpretation is rarely needed (see also ~ df-ral ).
+     (Contributed by NM, 30-Aug-1993.) $)
   df-rex $a |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) ) $.
 
-  $( Define restricted existential uniqueness.  (Contributed by NM,
-     22-Nov-1994.) $)
+  $( Define restricted existential uniqueness.
+
+     Note:  This notation is most often used to express that ` ph ` holds for
+     exactly one element of a given class ` A ` .  For this reading ` F/_ x A `
+     is required, though, for example, asserted when ` x ` and ` A ` are
+     disjoint.
+
+     Should instead ` A ` depend on ` x ` , you rather assert exactly one ` x `
+     fulfilling ` ph ` happens to be contained in the corresponding
+     ` A ( x ) ` .  This interpretation is rarely needed (see also ~ df-ral ).
+     (Contributed by NM, 22-Nov-1994.) $)
   df-reu $a |- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) ) $.
 
-  $( Define restricted "at most one".  (Contributed by NM, 16-Jun-2017.) $)
+  $( Define restricted "at most one".
+
+     Note:  This notation is most often used to express that ` ph ` holds for
+     at most one element of a given class ` A ` .  For this reading ` F/_ x A `
+     is required, though, for example, asserted when ` x ` and ` A ` are
+     disjoint.
+
+     Should instead ` A ` depend on ` x ` , you rather assert at most one ` x `
+     fulfilling ` ph ` happens to be contained in the corresponding
+     ` A ( x ) ` .  This interpretation is rarely needed (see also ~ df-ral ).
+     (Contributed by NM, 16-Jun-2017.) $)
   df-rmo $a |- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) ) $.
 
   $( Define a restricted class abstraction (class builder), which is the class
      of all ` x ` in ` A ` such that ` ph ` is true.  Definition of
-     [TakeutiZaring] p. 20.  (Contributed by NM, 22-Nov-1994.) $)
+     [TakeutiZaring] p. 20.
+
+     Note:  For the reading given above ` F/_ x A ` is required, though, for
+     example, asserted when ` x ` and ` A ` are disjoint.
+
+     Should instead ` A ` depend on ` x ` , you rather get a class of all those
+     ` x ` fulfilling ` ph ` that happen to be contained in the corresponding
+     ` A ( x ) ` .  This need not be a subset of any of the ` A ( x ) ` at all.
+     Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
+     by NM, 22-Nov-1994.) $)
   df-rab $a |- { x e. A | ph } = { x | ( x e. A /\ ph ) } $.
 
   $( Cancellation law for restricted universal quantification.  (Contributed by