From efe6b854078777bb389e5b3cc3558272315e62ad Mon Sep 17 00:00:00 2001
From: Benoit Jubin <benoit.jubin@gmail.com>
Date: Thu, 17 Aug 2023 23:45:25 +0200
Subject: [PATCH] taking review into account

---
 set.mm | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/set.mm b/set.mm
index c0b7d7019..5f7011fbd 100644
--- a/set.mm
+++ b/set.mm
@@ -24945,8 +24945,8 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
        is called "class extensionality".  Remark: the proof uses ~ axext4 to
        prove also the hypothesis of ~ df-cleq that is a degenerate instance,
        but it could be proved also from minimal propositional calculus and {
-       ~ ax-gen , ~ ax-4 }.  (Contributed by NM, 15-Sep-1993.)  (Revised by BJ,
-       24-Jun-2019.) $)
+       ~ ax-gen , ~ ax-4 , ~ equid }.  (Contributed by NM, 15-Sep-1993.)
+       (Revised by BJ, 24-Jun-2019.) $)
     dfcleq $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $=
       ( vy vz vv vu vt axext4 df-cleq ) ADEFGHBCDEGIHHFIJ $.
     $( $j usage 'dfcleq' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'ax-13'
@@ -25613,14 +25613,13 @@ the definition of class equality ( ~ df-cleq ).  Its forward implication
   ${
     $d z x $.  $d z y $.  $d z A $.
     $( Weaker version of ~ eleq1 (but more general than ~ elequ1 ) not
-       depending on ~ ax-ext nor ~ df-cleq .  Note that this proof does not
-       depend on ~ ax-8 (while ~ eleq2w depends on ~ ax-9 ), so this also gives
-       a proof of ~ ax-8 from Tarski's FOL and ~ dfclel (simply consider an
-       instance where ` A ` is replaced by a setvar and deduce the forward
-       implication by ~ biimpd ), which shows that ~ dfclel is too powerful to
-       be used a definition instead of ~ df-clel . taking an instance of the
-       forward implication where a setvar is substituted for ` A ` (Contributed
-       by BJ, 24-Jun-2019.) $)
+       depending on ~ ax-ext nor ~ df-cleq .
+
+       Note that this provides a proof of ~ ax-8 from Tarski's FOL and ~ dfclel
+       (simply consider an instance where ` A ` is replaced by a setvar and
+       deduce the forward implication by ~ biimpd ), which shows that ~ dfclel
+       is too powerful to be used as a definition instead of ~ df-clel .
+       (Contributed by BJ, 24-Jun-2019.) $)
     eleq1w $p |- ( x = y -> ( x e. A <-> y e. A ) ) $=
       ( vz weq cv wcel wa wex equequ2 anbi1d exbidv dfclel 3bitr4g ) ABEZDAEZDF
       CGZHZDIDBEZQHZDIAFZCGBFZCGORTDOPSQABDJKLDUACMDUBCMN $.