janitorial work: add references to similar theorems (#3797)

set.mm

@@ -27222,7 +27222,8 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
   ${
     $d w x $.  $d w A $.  $d w y $.
     clelsb3f.1 $e |- F/_ x A $.
-    $( Substitution applied to an atomic wff (class version of ~ elsb3 ).
+    $( Substitution applied to an atomic wff (class version of ~ elsb3 ).  See
+       ~ clelsb3fw not requiring ~ ax-13 , but extra disjoint variables.
        (Contributed by Rodolfo Medina, 28-Apr-2010.)  (Proof shortened by
        Andrew Salmon, 14-Jun-2011.)  (Revised by Thierry Arnoux, 13-Mar-2017.)
        (Proof shortened by Wolf Lammen, 7-May-2023.) $)
@@ -31321,18 +31322,21 @@ Such interpretation is rarely needed (see also ~ df-ral ).  (Contributed
     $d x A $.  $d y A $.  $d y ph $.  $d x ps $.
     cbvralv.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
     $( Change the bound variable of a restricted universal quantifier using
-       implicit substitution.  (Contributed by NM, 28-Jan-1997.) $)
+       implicit substitution.  See ~ cbvralvw based on fewer axioms , but extra
+       disjoint variables.  (Contributed by NM, 28-Jan-1997.) $)
     cbvralv $p |- ( A. x e. A ph <-> A. y e. A ps ) $=
       ( nfv cbvral ) ABCDEADGBCGFH $.
 
     $( Change the bound variable of a restricted existential quantifier using
-       implicit substitution.  (Contributed by NM, 2-Jun-1998.) $)
+       implicit substitution.  See ~ cbvrexvw based on fewer axioms , but extra
+       disjoint variables.  (Contributed by NM, 2-Jun-1998.) $)
     cbvrexv $p |- ( E. x e. A ph <-> E. y e. A ps ) $=
       ( nfv cbvrex ) ABCDEADGBCGFH $.
 
     $( Change the bound variable of a restricted unique existential quantifier
-       using implicit substitution.  (Contributed by NM, 5-Apr-2004.)  (Revised
-       by Mario Carneiro, 15-Oct-2016.) $)
+       using implicit substitution.  See ~ cbvreuvw for a version without
+       ~ ax-13 , but extra disjoint variables.  (Contributed by NM,
+       5-Apr-2004.)  (Revised by Mario Carneiro, 15-Oct-2016.) $)
     cbvreuv $p |- ( E! x e. A ph <-> E! y e. A ps ) $=
       ( nfv cbvreu ) ABCDEADGBCGFH $.