Hello, by reading axext (hol.mm theorem - http://us.metamath.org/holuni/axext.html) and ax-ext (axiom set.mm - http://us.metamath.org/mpeuni/ax-ext.html),
ax-ext $a |- ( A. z ( z e. x <-> z e. y ) -> x = y ) $. $d x y A $. $d x y B $. $d x y al $. axext.1 $e |- A : ( al -> bool ) $. axext.2 $e |- B : ( al -> bool ) $. $( Axiom of Extensionality. An axiom of Zermelo-Fraenkel set theory. It states that two sets are identical if they contain the same elements. Axiom Ext of [BellMachover] p. 461. $) axext $p |- T. |= [ ( ! x : al . [ ( A x : al ) = ( B x : al ) ] ==> [ A = B ] $= I have the impression that axext is not quite the HOL version of the extensionality axiom. Indeed, for me alpha->star is not necessary a set but only a predicate. So alpha->star would not always be a set but it could be a class. Also, ax-ext uses "=" and axext "<->". Is this difference important? Most likely, I probably misunderstood one or more concepts. Your help will be useful. RC -- 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/df127066-035e-4ce4-b6c6-263daf423680n%40googlegroups.com.
