Mathbox for Wolf Lammen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-wl-ral Structured version   Visualization version   GIF version

Definition df-wl-ral 35000
 Description: The definiens of df-ral 3114, ∀𝑥(𝑥 ∈ 𝐴 → 𝜑) 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 35001). If 𝑥 is not free in 𝐴, a simplification is possible ( see wl-dfralf 35003, wl-dfralv 35005). (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
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wl-ral 34995 . 2 wff ∀(𝑥 : 𝐴)𝜑
5 vy . . . . . 6 setvar 𝑦
65cv 1537 . . . . 5 class 𝑦
76, 3wcel 2112 . . . 4 wff 𝑦𝐴
82, 5weq 1964 . . . . . 6 wff 𝑥 = 𝑦
98, 1wi 4 . . . . 5 wff (𝑥 = 𝑦𝜑)
109, 2wal 1536 . . . 4 wff 𝑥(𝑥 = 𝑦𝜑)
117, 10wi 4 . . 3 wff (𝑦𝐴 → ∀𝑥(𝑥 = 𝑦𝜑))
1211, 5wal 1536 . 2 wff 𝑦(𝑦𝐴 → ∀𝑥(𝑥 = 𝑦𝜑))
134, 12wb 209 1 wff (∀(𝑥 : 𝐴)𝜑 ↔ ∀𝑦(𝑦𝐴 → ∀𝑥(𝑥 = 𝑦𝜑)))
 Colors of variables: wff setvar class This definition is referenced by:  wl-dfralsb  35001  wl-dfralf  35003  wl-dfralv  35005  wl-dfrexex  35014
 Copyright terms: Public domain W3C validator