Theorem wl-cleq-0 38001

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

Three specific theorems are under focus in the following pages: df-cleq 2757, df-clel 2840, and df-clab 2744. Only technical concepts necessary to explain these will be introduced, along with a selection of supporting theorems. The three theorems are central to a bootstrapping process that introduces objects into set.mm. We will first examine how Metamath in general creates basic new ideas from scratch, and then look at how these methods are applied specifically to classes, capable of representing objects in set theory.

In Zermelo-Fraenkel set theory with the axiom of choice (ZFC), these three theorems are (more or less) independent of each other, 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. Reordering theorems, though syntactically possible, sometimes may cause doubts when intermediate results are not strictly tied to ZFC only.

The purpose of set.mm is to provide a formal framework capable of proving the results of 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 another variant of set theory. This openess is already visible in axiom ax-mp 5, 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.

(Contributed by Wolf Lammen, 28-Sep-2025.)

Assertion

Ref	Expression
wl-cleq-0	⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-cleq-0

Step	Hyp	Ref	Expression
1		dfcleq 2758	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 209  ∀wal 1561   = wceq 1563   ∈ wcel 2145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757

This theorem is referenced by: (None)