rewrap

set.mm

@@ -30373,8 +30373,8 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     cbvrexfw.5 $e |- ( x = y -> ( ph <-> ps ) ) $.
     $( Rule used to change bound variables, using implicit substitution.
        Version of ~ cbvrexf with a disjoint variable condition, which does not
-       require ~ ax-13 .  For a version not dependent on ~ ax-11 and ax-12,
-       see ~ cbvrexvw .  (Contributed by FL, 27-Apr-2008.)  Avoid ~ ax-10 ,
+       require ~ ax-13 .  For a version not dependent on ~ ax-11 and ax-12, see
+       ~ cbvrexvw .  (Contributed by FL, 27-Apr-2008.)  Avoid ~ ax-10 ,
        ~ ax-13 .  (Revised by Gino Giotto, 10-Jan-2024.) $)
     cbvrexfw $p |- ( E. x e. A ph <-> E. y e. A ps ) $=
       ( wrex wn wral nfn weq notbid cbvralfw ralnex 3bitr3i con4bii ) ACEKZBDEK
@@ -30511,8 +30511,8 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     $d z x A $.  $d y A $.  $d z y ph $.  $d x y $.
     $( Change bound variable by using a substitution.  Version of ~ cbvralsv
        with a disjoint variable condition, which does not require ~ ax-13 .
-       (Contributed by NM, 20-Nov-2005.)  Avoid ~ ax-13 .  (Revised by Gino Giotto,
-       10-Jan-2024.) $)
+       (Contributed by NM, 20-Nov-2005.)  Avoid ~ ax-13 .  (Revised by Gino
+       Giotto, 10-Jan-2024.) $)
     cbvralsvw $p |- ( A. x e. A ph <-> A. y e. A [ y / x ] ph ) $=
       ( vz wral wsb nfv nfs1v sbequ12 cbvralw sbequ bitri ) ABDFABEGZEDFABCGZCD
       FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $.
@@ -30523,8 +30523,8 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     $d z x A $.  $d y z ph $.  $d y A $.  $d x y $.
     $( Change bound variable by using a substitution.  Version of ~ cbvrexsv
        with a disjoint variable condition, which does not require ~ ax-13 .
-       (Contributed by NM, 2-Mar-2008.)  Avoid ~ ax-13 .  (Revised by Gino Giotto,
-       10-Jan-2024.) $)
+       (Contributed by NM, 2-Mar-2008.)  Avoid ~ ax-13 .  (Revised by Gino
+       Giotto, 10-Jan-2024.) $)
     cbvrexsvw $p |- ( E. x e. A ph <-> E. y e. A [ y / x ] ph ) $=
       ( vz wrex wsb nfv nfs1v sbequ12 cbvrexw sbequ bitri ) ABDFABEGZEDFABCGZCD
       FANBEDAEHABEIABEJKNOECDNCHOEHAECBLKM $.