Theorem wl-cleq-2 37860

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 definite statements, open to doubt, alternatives, and reinterpretation.

Vocabulary

Sentence:
A sentence or closed form theorem is a theorem without any hypothesis, as opposed to the inference form. Although distinct variable conditions can be viewed as a particular kind of hypothesis, in Metamath they are treated as side conditions, and do not affect formal structure of the theorem. Expressions such as Ⅎ𝑥𝜑 or the distinctor ∀𝑥(𝑥 = 𝑦) play a similar role, but appear as separate hypotheses, or they can simply serve as the first antecedent in a sentence.

Bound / Free / Dependent:
In formal theories, variables are used to represent objects, allowing for general statements about relations rather than individual cases. In Metamath, for example, mathematical objects are represented by variables of type "setvar".

An occurrence of such a variable in any formula 𝜑 is said to be bound. if 𝜑 quantifies that variable, as in ∀𝑥𝜑. Variables not bound by a quantifier are called free. Variables of type "class" are always free, since quantifiers do not apply to them.

A free variable often indicates a parameter dependency; however, the formula 𝑥 = 𝑥 shows that this is not necessarily the case. In Metamath, a variable expressing a real dependency is also called "effectively free" (see nfequid 2020, with thanks to SN for pointing out this theorem).

Instance:
A formula of type "class" that is not a mere variable is called an instance of any "class" type variable. An instance may represent a single object, or it may still describe a family of objects, when variables expressing dependencies occur within that formula.

Attribute:
Objects possess properties, some of which may uniquely identify them. In logic, properties are also known as attributes. They are described by formulas depending on a variable, which can then be substituted with a specific object. If the resulting statement is true, that particular attribute is said to apply to the object.

Multiple objects forming an instance may share common attributes. A variable inherits the attributes of the instance it represents.

(Contributed by Wolf Lammen, 12-Oct-2025.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-cleq-2

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

Syntax hints:   ↔ wb 207  ∀wal 1545   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by: (None)