It seems like if one wants to define equality instead of "axiomizing" it, it would be as |- ( x = y <-> A. w ( w e. x <-> w e. y ) )
So I started doing a little digging to how much things would change if we used that instead. ax-7 |- ( x = y -> ( x = z -> y = z ) ) I think we can derive ax-7 by using the following theorems by definition |- ( x = y <-> A. w ( w e. x <-> w e. y ) ) using albiim, syl, some other biconditional theorems |- ( A. w ( w e. x <-> w e. y ) -> A. w ( w e. x -> w e. y ) ) |- ( A. w ( w e. x <-> w e. y ) -> A. w ( w e. y -> w e. x ) ) the same can be applied to x = z with that and a few other theorems (such as alsyl) I'm pretty sure you can reach |- ( ( A. w ( w e. x <-> w e. y ) /\ A. w ( w e. x <-> w e. z ) ) -> A. w ( w e. y <-> w e. z ) ) and applying ex we can prove ax-7 The description in the axiom of extensionality already states that if we define equality instead axiomizing it, we can basically rewrite it as ax-8. So that's covered Unfortunately, we can't prove ax-9 with this definition without ax-12 But using ax-12, we can pretty much apply sp to the definition, along with biimp and syl and that proves ax-9 So us there another reason to why it's preferable to use equality as a primitive wff? There's a chance I'm forgetting problems that could arise, or maybe it's just really inconvenient in the long run. -- 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/ca90429b-d941-4e6f-8feb-6e33e4b8d245n%40googlegroups.com.
