Minor

Deletet "Alternate" form "Alternate elimination".
metamath · Jan 12, 2025 · 566ecee · 566ecee
1 parent 8a8e0be
commit 566ecee
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/set.mm b/set.mm
@@ -33835,8 +33835,8 @@ general is seen either by substitution (when the variable ` V ` has no
       wb rexbiia pm5.32i 3bitr3i ) DEGZCHZDIZAJZJZCEKUCUFCEKZJUHUCBJUCUFCELUGUF
       CEUGUDEGZUFUIUFJUGUFUIUCUEUIUCSAUDDEMNOPQTUCUHBABCDEFRUAUB $.
 
-    $( Alternate elimination of a restricted universal quantifier, using
-       implicit substitution.  (Contributed by Scott Fenton, 7-Dec-2020.) $)
+    $( Elimination of a restricted universal quantifier, using implicit
+       substitution.  (Contributed by Scott Fenton, 7-Dec-2020.) $)
     ceqsralbv $p |- ( A. x e. B ( x = A -> ph ) <-> ( A e. B -> ps ) ) $=
       ( cv wceq wi wral wcel wn wa wrex notbid ceqsrexbv rexanali annim 3bitr3i
       con4bii ) CGDHZAICEJZDEKZBIZUAALZMCENUCBLZMUBLUDLUEUFCDEUAABFOPUAACEQUCBR