Mario would be the best person to answer this, but I've noticed myself that
DV conditions in MM1 don't quite behave in the same way as in Metamath. In
Metamath, you can prove the statement of the full ax-8 by exploiting
alpha-renaming of certain definitions (see in-ax8
<https://us.metamath.org/mpeuni/in-ax8.html> and ss-ax8
<https://us.metamath.org/mpeuni/ss-ax8.html>). However, in MM1, it seems
that deriving the full ax-8 is not possible, and the best we can do is to
derive a weaker version of ax-8 with bound variables (see this discussion
<https://groups.google.com/g/metamath/c/WXvL9xfaR9U> if you want to enter
this rabbit hole):
theorem ax8vvv {a b: set} (c: set): $ a =s b -> a es. c -> b es. c $).
Anyway, this is an example that some unbundling proofs that work in
Metamath do not work in MM1, and this is probably by design. After all, it
would be strange if the "hidden axiom schema" that Mario mentions in his
post <https://groups.google.com/g/metamath/c/WXvL9xfaR9U/m/Q52iEo8TAAAJ>,
meant to govern bound variables, allowed the user to derive theorems that
contain no bound variables at all.
Regarding your specific question, the purpose of the proof of ax7
<https://us.metamath.org/mpeuni/ax7.html> is to "unbundle" ax-7 (see this
post <https://groups.google.com/g/metamath/c/ahysZRWoMHw/m/SmjTXb-KBAAJ>),
which means deriving the full version of ax-7 (the one with no DV
conditions) from weaker ones (with DV conditions). So, I think what you are
trying to do here is to replicate the unbundling process in MM1.
Here is a version that works:
theorem ax7v1 {x: set} (y z: set): $ x =s y -> x =s z -> y =s z $ = 'ax_7;
theorem ax7v2 {y: set} (x z: set): $ x =s y -> x =s z -> y =s z $ = 'ax_7;
theorem ax7 (x y z: set): $ x =s y -> x =s z -> y =s z $
= '(exlimiiv (equcoms (syld ax7v2 (com23 (syld ax7v2 (a1i (com12
ax7v1))))))
(!! ax6ev w));
I took the names of the used theorems from set.mm, so you should be able to
replicate the proof. The generated ax7 has no bound variables at all, and
it's identical to the original ax-7. This is problably the closest you can
get to the Metamath version of unbundling ax-7. It makes intuitive sense
since the Metamath version ax7v1 <https://us.metamath.org/mpeuni/ax7v1.html>
has the DVs $ x y $ and $ x z $, which seems to coincide to how this MM1
version ax7v1 behaves:
theorem ax7v1_dgen1 {x: set} (z: set): $ x =s x -> x =s z -> x =s z $ = '
ax7v1; --> gives an error: disjoint variable violation at ax7v1 (x, y) ->
(x, x)
theorem ax7v1_dgen2 {x: set} (y: set): $ x =s y -> x =s x -> y =s x $ = '
ax7v1; --> gives an error: disjoint variable violation at ax7v1 (x, z) ->
(x, x)
theorem ax7v1_dgen3 {x: set} (y: set): $ x =s y -> x =s y -> y =s y $ = '
ax7v1; --> does not give an error (y and z are not disjoint)
You can do an analogous check for ax7v2
<https://us.metamath.org/mpeuni/ax7v2.html>, which has the DVs $ x y $ and
$ y z $. You might encounter similar issues when unbundling ax-8 and ax-9
as well.
Il giorno martedì 5 maggio 2026 alle 21:09:26 UTC+2 [email protected] ha
scritto:
> I agree that ax7v does have some form of "binding" for z from x and that
> ax7 does not. However, because ax7 depends on ax7v, it requires x to be
> bound regardless of what the outcome is.
>
> I've also read that part of the documentation, like I stated originally,
> but "Variable Inference" is not a section in the current version of the
> documentation, and the old documentation has outdated syntax.
> On Tuesday, May 5, 2026 at 1:31:53 PM UTC-4 [email protected] wrote:
>
>> From my vague understanding, I think that none of the variables in
>>
>> `theorem ax7{x y z .t: setvar}: $ x =s y -> x =s z -> y =s z $`
>> are bound to each other. They are all of type "setvar", and this type
>> does not depend on any variable. So no actual binding is happening, despite
>> all the variables being a "bound variable".
>>
>> Contrast with
>>
>> `theorem ax7v{x: setvar} (y: setvar) (z: setvar x): $ x =s y -> x =s z ->
>> y =s z $ = 'ax_7;`
>> where z's type depends on x, so x is ..."actively" bound or something
>>
>>
>> Relevant part of the documentation
>> https://github.com/digama0/mm0/blob/master/mm0.md: A binder enclosed in
>> curly braces as in `{x: set}` denotes a bound variable, which may appear in
>> dependencies of other types (see "Variable Inference").
>>
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/7e4ea44d-7bdc-4ec1-b3d4-87827e8a8fbdn%40googlegroups.com.
