Theorem wl-cleq-0 37481

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 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.

In particular, the three theorems df-clab 2718, df-cleq and df-clel 2819 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.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-cleq-0

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

Syntax hints:   ↔ wb 206  ∀wal 1535   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by: (None)