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 x | A y |

Proof

Step Hyp Ref Expression
1 bj-denoteslem z z = A A x |
2 bj-denoteslem z z = A A y |
3 1 2 bitr3i A x | A y |