Theorem wl-cleq-2 37741

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 2015, 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 2730	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 206  ∀wal 1540   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by: (None)