Hypotheses with an "is a set" property using the universal class _V

[avekens]

Hypotheses with an "is a set" property using the universal class _V

[tirix]

I agree with the direction here.

You might think about #944 ?

[avekens]

#944 is about '( ? e. _V -> ' , that means e. _V is used in the antecedent of an implication, not as consequent (of a hypothesis) as mentioned above.

[tirix]

#944 is about '( ? e. _V -> ' , that means e. _V is used in the antecedent of an implication, not as consequent (of a hypothesis) as mentioned above.

Indeed!
I don't remember any other such discussion, and could not find any when searching.

[jkingdon]

Sounds like a good change to me. If you are able to get to it, doing this in iset.mm as well would be appreciated. Because iset.mm has https://us.metamath.org/ileuni/elex.html and other theorems relevant to this discussion, the tradeoffs in iset.mm are the same as in set.mm.