Description: A form of elequ2 with a universal quantifier. Its converse is the axiom of extensionality ax-ext . (Contributed by BJ, 3-Oct-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | elequ2g | |- ( x = y -> A. z ( z e. x <-> z e. y ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elequ2 | |- ( x = y -> ( z e. x <-> z e. y ) ) |
|
2 | 1 | alrimiv | |- ( x = y -> A. z ( z e. x <-> z e. y ) ) |