rewrap

metamath · Nov 18, 2024 · b29b64a · b29b64a
1 parent 2c76746
commit b29b64a
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/set.mm b/set.mm
@@ -81542,9 +81542,9 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $=
       SUNUOUDUEABCDUFUGZECABDUHABUSUIFABDUJUKULUM $.
     $( $j usage 'wfrresex' avoids 'ax-rep'; $)
 
-    $( A weak version of ~ wfr2 which is useful for proofs that avoid the
-       Axiom of Replacement.  (Contributed by Scott Fenton, 30-Jul-2020.)
-       (Proof shortened by Scott Fenton, 18-Nov-2024.) $)
+    $( A weak version of ~ wfr2 which is useful for proofs that avoid the Axiom
+       of Replacement.  (Contributed by Scott Fenton, 30-Jul-2020.)  (Proof
+       shortened by Scott Fenton, 18-Nov-2024.) $)
     wfr2a $p |- ( ( ( R We A /\ R Se A ) /\ X e. dom F ) ->
     ( F ` X ) = ( G ` ( F |` Pred ( R , A , X ) ) ) ) $=
       ( wwe wse wa cdm wcel cfv cpred cres c2nd ccom co wfr adantr simpr cwrecs