|Description: The definiens of df-ral 3110, ∀𝑥(𝑥 ∈ 𝐴 → 𝜑) is a short and
simple expression, but has a severe downside: It allows for two
substantially different interpretations. One, and this is the common
case, wants this expression to denote that 𝜑 holds for all elements
of 𝐴. To this end, 𝑥 must
not be free in 𝐴, though .
Should instead 𝐴 vary with 𝑥, then we rather focus on
𝑥, that happen to be an element of
their respective 𝐴(𝑥).
Such interpretation is rare, but must nevertheless be considered in
design and comments.
In addition, many want definitions be designed to express just a single
idea, not many.
Our definition here introduces a dummy variable 𝑦, disjoint from
all other variables, to describe an element in 𝐴. It lets 𝑥
appear as a formal parameter with no connection to 𝐴, but
occurrences in 𝜑 are still honored.
The resulting subexpression ∀𝑥(𝑥 = 𝑦 → 𝜑) is [𝑦 / 𝑥]𝜑
in disguise (see wl-dfralsb 34387).
If 𝑥 is not free in 𝐴, a simplification is
possible ( see
wl-dfralf 34389, wl-dfralv 34391). (Contributed by NM, 19-Aug-1993.)
x from A, idea of Mario Carneiro. (Revised by Wolf Lammen,