Prove ax-8 from df-ss (#4995)

* ax-8 from df-ss

* discouraged

Author: GinoGiotto

discouraged

@@ -16964,7 +16964,6 @@ New usage of "genpnnp" is discouraged (1 uses).
 New usage of "genpprecl" is discouraged (8 uses).
 New usage of "genpss" is discouraged (1 uses).
 New usage of "genpv" is discouraged (3 uses).
-New usage of "gg-ax8" is discouraged (0 uses).
 New usage of "ggen22" is discouraged (0 uses).
 New usage of "ggen31" is discouraged (2 uses).
 New usage of "ghomidOLD" is discouraged (2 uses).
@@ -17537,6 +17536,7 @@ New usage of "imsmet" is discouraged (12 uses).
 New usage of "imsmetlem" is discouraged (1 uses).
 New usage of "imsval" is discouraged (5 uses).
 New usage of "imsxmet" is discouraged (15 uses).
+New usage of "in-ax8" is discouraged (0 uses).
 New usage of "in1" is discouraged (89 uses).
 New usage of "in2" is discouraged (36 uses).
 New usage of "in2an" is discouraged (1 uses).
@@ -19454,6 +19454,7 @@ New usage of "srhmsubcALTV" is discouraged (4 uses).
 New usage of "srhmsubcALTVlem1" is discouraged (2 uses).
 New usage of "srhmsubcALTVlem2" is discouraged (1 uses).
 New usage of "sringcatALTV" is discouraged (2 uses).
+New usage of "ss-ax8" is discouraged (0 uses).
 New usage of "ssctOLD" is discouraged (0 uses).
 New usage of "ssdmd1" is discouraged (1 uses).
 New usage of "ssdmd2" is discouraged (0 uses).
@@ -21021,7 +21022,6 @@ Proof modification of "gen21" is discouraged (16 steps).
 Proof modification of "gen21nv" is discouraged (18 steps).
 Proof modification of "gen22" is discouraged (23 steps).
 Proof modification of "gen31" is discouraged (19 steps).
-Proof modification of "gg-ax8" is discouraged (208 steps).
 Proof modification of "ggen22" is discouraged (13 steps).
 Proof modification of "ggen31" is discouraged (22 steps).
 Proof modification of "ghomidOLD" is discouraged (178 steps).
@@ -21101,6 +21101,7 @@ Proof modification of "impsingle-step22" is discouraged (50 steps).
 Proof modification of "impsingle-step25" is discouraged (45 steps).
 Proof modification of "impsingle-step4" is discouraged (75 steps).
 Proof modification of "impsingle-step8" is discouraged (133 steps).
+Proof modification of "in-ax8" is discouraged (208 steps).
 Proof modification of "in1" is discouraged (11 steps).
 Proof modification of "in2" is discouraged (10 steps).
 Proof modification of "in2an" is discouraged (18 steps).
@@ -21685,6 +21686,7 @@ Proof modification of "sratsetOLD" is discouraged (21 steps).
 Proof modification of "sravscaOLD" is discouraged (177 steps).
 Proof modification of "srgcom4" is discouraged (279 steps).
 Proof modification of "srgcom4lem" is discouraged (213 steps).
+Proof modification of "ss-ax8" is discouraged (243 steps).
 Proof modification of "ssctOLD" is discouraged (38 steps).
 Proof modification of "sseliALT" is discouraged (152 steps).
 Proof modification of "ssfiALT" is discouraged (222 steps).

set.mm

@@ -579263,11 +579263,11 @@ conditions of the Five Segment Axiom ( ~ ax5seg ).  See ~ brofs and
     $d x t w $.  $d y t w $.  $d z t w $.
     $( A proof of ~ ax-8 that does not rely on ~ ax-8 .  It employs ~ df-in to
        perform alpha-renaming and eliminates disjoint variable conditions using
-       dummy variables.  Since the nature of this result is unclear, usage of
-       this theorem is discouraged, and this method should not be applied to
+       ~ ax-9 .  Since the nature of this result is unclear, usage of this
+       theorem is discouraged, and this method should not be applied to
        eliminate axiom dependencies.  (Contributed by GG, 1-Aug-2025.)
        (Proof modification is discouraged.)  (New usage is discouraged.) $)
-    gg-ax8 $p |- ( x = y -> ( x e. z -> y e. z ) ) $=
+    in-ax8 $p |- ( x = y -> ( x e. z -> y e. z ) ) $=
       ( vt vw weq wel wi wa wal wsb sb6 cv cab wcel df-in df-clab equcoms ax6ev
       exlimiiv ax7 ax12v2 imp wb wceq cin eqtr3i dfcleq mpbi spi 3bitr3i bitr3i
       sylbb sp 3syl ex com23 sylcom com12 pm4.24 3imtr4g ax9 imim12d syl5 ) DCF
@@ -579276,7 +579276,27 @@ conditions of the Five Segment Axiom ( ~ ax5seg ).  See ~ brofs and
       MBEKZVTVSVLAEKZWAVLAELEMZVLANZOZWCVMBNZOZWBWAWEWGUDZEWDWFUEWHEJDMZWIUFWDW
       FAWIWIPBWIWIPUGEWDWFUHUIUJVLEAQVMEBQUKULVMBELUMVRBUNUOUPUQURUSREASTVJUTVK
       UTVAVEVGVJVKVHVGVJHCDCDAVBRDCBVBVCVDDCST $.
-    $( $j usage 'gg-ax8' avoids 'ax-8' 'df-clel'; $)
+    $( $j usage 'in-ax8' avoids 'ax-8' 'df-clel'; $)
+  $}
+
+  ${
+    $d x t w v $.  $d y t w v $.  $d z t w v $.
+    $( A proof of ~ ax-8 that does not rely on ~ ax-8 .  It employs ~ df-ss to
+       perform alpha-renaming and eliminates disjoint variable conditions using
+       ~ ax-9 .  Contrary to ~ in-ax8 , this proof does not rely on ~ df-cleq ,
+       therefore using fewer axioms .  This method should not be applied to
+       eliminate axiom dependencies.  (Contributed by GG, 30-Aug-2025.)
+       (Proof modification is discouraged.)  (New usage is discouraged.) $)
+    ss-ax8 $p |- ( x = y -> ( x e. z -> y e. z ) ) $=
+      ( vt vw vv weq wel wi wal wsb equsb3 bicomi imbi1i albii cv df-clab df-ss
+      wcel 3bitri ax7 wa ax12v2 imp cab wss bitr3i biimpi sp com23 sylcom com12
+      3syl ex equcoms ax6ev exlimiiv ax9 imim12d syl5 ) DCGZABGZACHZBCHZIZIDVBA
+      DHZBDHZIZVAVEEAGVBVHIZEVIAEVBAEGZVHVBVJBEGZVHABEUAVJVFVKVGVJVFVKVGIZVJVFU
+      BVJVFIZAJZVLBJZVLVJVFVNVFAEUCUDVNVOVNFEGZFAKZVFIZAJZVPFBKZVGIZBJZVOVMVRAV
+      JVQVFVQVJFAELMNOVSAPZVPFUEZSZVFIZAJBPZWDSZVGIZBJWBVRWFAVQWEVFWEVQVPAFQMNO
+      WEWCDPZSIAJWDWJUFWHWGWJSIBJAWDWJRBWDWJRUGWIWABWHVTVGVPBFQNOTWAVLBVTVKVGFB
+      ELNOTUHVLBUIUMUNUJUKULUOEAUPUQVAVCVFVGVDVCVFICDCDAURUODCBURUSUTDCUPUQ $.
+    $( $j usage 'ss-ax8' avoids 'ax-8' 'ax-ext' 'df-clel' 'df-cleq'; $)
   $}