Theorem wl-cleq-2

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.

Sentence:
Asentence orclosed 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 F/ x ph or the distinctor A. x ( x = y ) 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 ph is said to be bound. if ph quantifies that variable, as in A. x ph . 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 x = x shows that this is not necessarily the case. In Metamath, a variable expressing a real dependency is also called "effectively free" (see nfequid , 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)

	Ref	Expression
Assertion	wl-cleq-2	$$⊢A=B\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfcleq	$$⊢A=B\leftrightarrow \forall x\left(x\in A\leftrightarrow x\in B\right)$$