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 issettru ⊢ ∃ z z = A ↔ A ∈ x | ⊤
2 issettru ⊢ ∃ z z = A ↔ A ∈ y | ⊤
3 1 2 bitr3i ⊢ A ∈ x | ⊤ ↔ A ∈ y | ⊤