> I've referenced it a few times in this conversation as a hypothetical > axiom extending ax-9 to classes: x = y -> (x e. A -> y e. A). >
This looks more like "ax-8c" , aka http://us.metamath.org/mpeuni/bj-eleq1w.html Mario: why, when you encounter a dummy class variable in the original proof, don't you simply use a dummy setvar variable in place of it ? Your proof is more or less what I was trying to write up, but I hadn't seen some of the subtleties... Maybe I'll come back with further questions. Benoît -- 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 on the web visit https://groups.google.com/d/msgid/metamath/ebb9d9e4-e9b2-413d-ac6a-e28f4ab51e42n%40googlegroups.com.
