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)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-elabtru | ⊢ ( 𝐴 ∈ { 𝑥 ∣ ⊤ } ↔ 𝐴 ∈ { 𝑦 ∣ ⊤ } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-denoteslem | ⊢ ( ∃ 𝑧 𝑧 = 𝐴 ↔ 𝐴 ∈ { 𝑥 ∣ ⊤ } ) | |
2 | bj-denoteslem | ⊢ ( ∃ 𝑧 𝑧 = 𝐴 ↔ 𝐴 ∈ { 𝑦 ∣ ⊤ } ) | |
3 | 1 2 | bitr3i | ⊢ ( 𝐴 ∈ { 𝑥 ∣ ⊤ } ↔ 𝐴 ∈ { 𝑦 ∣ ⊤ } ) |