Definition df-wl-ral 34386

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 those 𝑥, 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.) Isolate x from A, idea of Mario Carneiro. (Revised by Wolf Lammen, 21-May-2023.)

Assertion

Ref	Expression
df-wl-ral	⊢ (∀(𝑥 : 𝐴)𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Detailed syntax breakdown of Definition df-wl-ral

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wl-ral 34381	. 2 wff ∀(𝑥 : 𝐴)𝜑
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1521	. . . . 5 class 𝑦
7	6, 3	wcel 2081	. . . 4 wff 𝑦 ∈ 𝐴
8	2, 5	weq 1941	. . . . . 6 wff 𝑥 = 𝑦
9	8, 1	wi 4	. . . . 5 wff (𝑥 = 𝑦 → 𝜑)
10	9, 2	wal 1520	. . . 4 wff ∀𝑥(𝑥 = 𝑦 → 𝜑)
11	7, 10	wi 4	. . 3 wff (𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
12	11, 5	wal 1520	. 2 wff ∀𝑦(𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
13	4, 12	wb 207	1 wff (∀(𝑥 : 𝐴)𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

This definition is referenced by:  wl-dfralsb  34387  wl-dfralf  34389  wl-dfralv  34391  wl-dfrexex  34400