Description: Disclaimer: The material presented here is just my (WL's) personal perception. I am not an expert in this field, so some or all of the text here can be misleading, or outright wrong.
This and the following texts should be read as explorations rather than as definite statements, open to doubt, alternatives, and reinterpretation.
**Preface**
The purpose of set.mm is to provide a formal framework capable of proving the results of Zermelo-Fraenkel set theory with the axiom of choice (ZFC), provided that formulas are properly interpreted. In fact, there is freedom of interpretation. The database set.mm develops from the very beginning, where nothing is assumed or fixed, and gradually builts up to the full abstraction of ZFC. Along the way, results are only preliminary, and one may at any point branch off and pursue a different path toward a variant of set theory.
This openess is already visible in axiom ax-mp , where the symbol -> can be understood as as implication, bi-conditional, or conjunction. The notation and symbol shapes are suggestive, but their interpretation is not mandatory.
The point here is that Metamath, as a purely syntactic system, can sometimes allow freedoms, unavailable to semantically fixed systems, which presuppose only a single ultimate goal.
In particular, the three theorems df-clab , df-cleq and df-clel will be the focus in what follows. In ZFC, these three are (more or less) independent, which means they can be introduced in different orders.
From my own experience, another order has pedagogical advantages: it helps grasping not only the overall concept better, but also the intricate details that I first found difficult to comprehend.
(Contributed by Wolf Lammen, 28-Sep-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-cleq-0 | ⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfcleq | ⊢ ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) |