shorten proofs (#4594)

* shorten cbeqsalv

* shorten ceqsexv

discouraged

@@ -15540,6 +15540,7 @@ New usage of "cdlemm10N" is discouraged (0 uses).
 New usage of "ceqsalgALT" is discouraged (0 uses).
 New usage of "ceqsalvOLD" is discouraged (0 uses).
 New usage of "ceqsexvOLD" is discouraged (0 uses).
+New usage of "ceqsexvOLDOLD" is discouraged (0 uses).
 New usage of "ceqsralvOLD" is discouraged (0 uses).
 New usage of "cgcdOLD" is discouraged (1 uses).
 New usage of "cghomOLD" is discouraged (13 uses).
@@ -20132,7 +20133,8 @@ Proof modification of "ccatw2s1p1OLD" is discouraged (155 steps).
 Proof modification of "cchhllemOLD" is discouraged (157 steps).
 Proof modification of "ceqsalgALT" is discouraged (58 steps).
 Proof modification of "ceqsalvOLD" is discouraged (10 steps).
-Proof modification of "ceqsexvOLD" is discouraged (10 steps).
+Proof modification of "ceqsexvOLD" is discouraged (47 steps).
+Proof modification of "ceqsexvOLDOLD" is discouraged (10 steps).
 Proof modification of "ceqsralvOLD" is discouraged (38 steps).
 Proof modification of "cgsex4gOLD" is discouraged (218 steps).
 Proof modification of "chordthmALT" is discouraged (440 steps).

set.mm

@@ -32350,8 +32350,8 @@ general is seen either by substitution (when the variable ` V ` has no
        inferred from an implicit substitution hypothesis.  (Contributed by NM,
        18-Aug-1993.)  Avoid ~ ax-12 .  (Revised by SN, 8-Sep-2024.) $)
     ceqsalv $p |- ( A. x ( x = A -> ph ) <-> ps ) $=
-      ( cv wceq wi wal wex pm5.74i albii 19.23v wb isseti pm5.5 ax-mp 3bitri )
-      CGDHZAIZCJTBIZCJTCKZBIZBUAUBCTABFLMTBCNUCUDBOCDEPUCBQRS $.
+      ( cv wceq wi wal wex 19.23v pm5.74i albii isseti a1bi 3bitr4i ) CGDHZBIZC
+      JRCKZBIRAIZCJBRBCLUASCRABFMNTBCDEOPQ $.
     $( $j usage 'ceqsalv' avoids 'ax-12'; $)
 
     $( Obsolete version of ~ ceqsalv as of 8-Sep-2024.  (Contributed by NM,
@@ -32519,22 +32519,29 @@ general is seen either by substitution (when the variable ` V ` has no
     ceqsexv.2 $e |- ( x = A -> ( ph <-> ps ) ) $.
     $( Elimination of an existential quantifier, using implicit substitution.
        (Contributed by NM, 2-Mar-1995.)  Avoid ~ ax-12 .  (Revised by Gino
-       Giotto, 12-Oct-2024.) $)
+       Giotto, 12-Oct-2024.)  (Proof shortened by Wolf Lammen, 22-Jan-2025.) $)
     ceqsexv $p |- ( E. x ( x = A /\ ph ) <-> ps ) $=
-      ( cv wceq wa wex biimpa exlimiv wal biimprcd alrimiv isseti exintr mpisyl
-      wi impbii ) CGDHZAIZCJZBUBBCUAABFKLBUAASZCMUACJUCBUDCUAABFNOCDEPUAACQRT
-      $.
+      ( cv wceq wa wex wn wi wal alinexa notbid ceqsalv bitr3i con4bii ) CGDHZA
+      ICJZBTKSAKZLCMBKZSACNUAUBCDESABFOPQR $.
     $( $j usage 'ceqsexv' avoids 'ax-10' 'ax-11' 'ax-12'; $)
   $}
 
   ${
     $d x A $.  $d x ps $.
     ceqsexvOLD.1 $e |- A e. _V $.
     ceqsexvOLD.2 $e |- ( x = A -> ( ph <-> ps ) ) $.
+    $( Obsolete version of ~ ceqsexv as of 12-Oct-2024.  (Contributed by NM,
+       2-Mar-1995.)  Avoid ~ ax-12 .  (Revised by Gino Giotto, 12-Oct-2024.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    ceqsexvOLD $p |- ( E. x ( x = A /\ ph ) <-> ps ) $=
+      ( cv wceq wa wex biimpa exlimiv wal biimprcd alrimiv isseti exintr mpisyl
+      wi impbii ) CGDHZAIZCJZBUBBCUAABFKLBUAASZCMUACJUCBUDCUAABFNOCDEPUAACQRT
+      $.
+
     $( Obsolete version of ~ ceqsexv as of 12-Oct-2024.  (Contributed by NM,
        2-Mar-1995.)  (Proof modification is discouraged.)
        (New usage is discouraged.) $)
-    ceqsexvOLD $p |- ( E. x ( x = A /\ ph ) <-> ps ) $=
+    ceqsexvOLDOLD $p |- ( E. x ( x = A /\ ph ) <-> ps ) $=
       ( nfv ceqsex ) ABCDBCGEFH $.
   $}