Metamath Proof Explorer


Theorem bj-elabtru

Description: This is as close as we can get to proving extensionality for "the" "universal" class without ax-ext . (Contributed by BJ, 24-Apr-2024) (Proof modification is discouraged.)

Ref Expression
Assertion bj-elabtru
|- ( A e. { x | T. } <-> A e. { y | T. } )

Proof

Step Hyp Ref Expression
1 bj-denoteslem
 |-  ( E. z z = A <-> A e. { x | T. } )
2 bj-denoteslem
 |-  ( E. z z = A <-> A e. { y | T. } )
3 1 2 bitr3i
 |-  ( A e. { x | T. } <-> A e. { y | T. } )