Theorem wl-cleq-0 38525

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 2752, df-clel 2835, and df-clab 2739. 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 2753	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1567   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by: (None)