Definition df-wl-ral 34881

Description: The definiens of df-ral 3142, ∀𝑥(𝑥 ∈ 𝐴 → 𝜑) 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 34882).

If 𝑥 is not free in 𝐴, a simplification is possible ( see wl-dfralf 34884, wl-dfralv 34886). (Contributed by NM, 19-Aug-1993.) Isolate 𝑥 from 𝐴, 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 34876	. 2 wff ∀(𝑥 : 𝐴)𝜑
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1535	. . . . 5 class 𝑦
7	6, 3	wcel 2113	. . . 4 wff 𝑦 ∈ 𝐴
8	2, 5	weq 1963	. . . . . 6 wff 𝑥 = 𝑦
9	8, 1	wi 4	. . . . 5 wff (𝑥 = 𝑦 → 𝜑)
10	9, 2	wal 1534	. . . 4 wff ∀𝑥(𝑥 = 𝑦 → 𝜑)
11	7, 10	wi 4	. . 3 wff (𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
12	11, 5	wal 1534	. 2 wff ∀𝑦(𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
13	4, 12	wb 208	1 wff (∀(𝑥 : 𝐴)𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))

This definition is referenced by:  wl-dfralsb  34882  wl-dfralf  34884  wl-dfralv  34886  wl-dfrexex  34895