From c1824c553c4d0bd247926cd009af6a81bbc7790e Mon Sep 17 00:00:00 2001
From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com>
Date: Thu, 10 Aug 2023 15:00:00 +0200
Subject: [PATCH] reduced ax-10 usage

---
 set.mm | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/set.mm b/set.mm
index 0d630c0df7..010f2ace1a 100644
--- a/set.mm
+++ b/set.mm
@@ -19024,7 +19024,8 @@ Corresponds to the dual of Axiom (B) of modal logic.  (Contributed by NM,
     $( Version of ~ cbv3 with a disjoint variable condition, which does not
        require ~ ax-13 .  (Contributed by BJ, 31-May-2019.) $)
     cbv3v $p |- ( A. x ph -> A. y ps ) $=
-      ( wal nfal spimv1 alrimi ) ACHBDADCEIABCDFGJK $.
+      ( wal nf5ri hbal weq wi ax6ev eximii 19.36i alrimih ) ACHBDADCADEIJABCFCD
+      KABLCCDMGNOP $.
   $}
 
   ${
@@ -19614,7 +19615,8 @@ theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10).  In the
        does not use ~ ax-c9 .  (Contributed by NM, 5-Aug-1993.)  (Proof
        shortened by Wolf Lammen, 12-May-2018.) $)
     cbv3 $p |- ( A. x ph -> A. y ps ) $=
-      ( wal nfal spim alrimi ) ACHBDADCEIABCDFGJK $.
+      ( wal nf5ri hbal weq wi ax6e eximii 19.36i alrimih ) ACHBDADCADEIJABCFCDK
+      ABLCCDMGNOP $.
   $}
 
   ${