Theorem wl-cleq-1 37482

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 text should be read as an exploration rather than as a definite statement, open to doubt, alternatives, and reinterpretation.

**Grammars and Parsable contents**

A Metamath program is a text-based tool. Its input consists of (mostly) human-readable and editable text stored in *.mm files. For automatic processing, these files follow a strict structure. This enables automated analysis of their contents, verification of proofs, proof assistance, and the generation of output files - for example, the HTML page of this dummy theorem. A set.mm file contains many such instructions serving these purposes.

The ideas presented here focus only on specific statements: df-cleq 2732, df-clel 2819, and df-clab 2718. Accordingly, only the technical concepts necessary to explain these are introduced, along with a selection of supporting theorems.

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

This page provides a brief explanation of the general concepts behind structured text such as that found in set.mm. As noted above, set.mm is written in a form that is readable by humans. However, for Metamath this is not sufficient: the program must also verify and process set.mm automatically in order to establish a high degree of confidence in its correctness.

When a text exhibits a sufficiently regular structure, its form can be described by a set of syntax rules, known as a grammar. Such rules are composed of terminal symbols (fixed, literal elements) and non-terminal symbols, which can recursively be expanded using the grammar's rewrite rules. A program component that applies a grammar to a text is called a parser. The parser decomposes the text into smaller parts, called syntactic units, while often maintaining contextual information. These units may then be handed over to subsequent components for further processing, such as populating a database or generating output.

In these pages, we restrict our attention to strictly formatted material consisting of formulas with logical and mathematical content. These syntactic units are embedded in higher-level structures such as chapters, together with commands that, for example, control the HTML output.

Conceptually, the parsing process can be viewed as consisting of two stages. The top-level stage applies a simple built-in grammar to identify its structural units. Each unit is a text region marked on both sides with predefined tokens (in Metamath: keywords), beginning with the escape character "$". Text regions containing logical or mathematical formulas are then passed to a second-stage parser, which applies a different grammar. Unlike the first, this grammar is not built-in but is dynamically constructed.

In what follows, we will ignore the first stage of parsing, since its role is only to extract the relevant material embedded within text primarily intended for human readers.

(Contributed by Wolf Lammen, 18-Aug-2025.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-cleq-1

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)