Definition df-wl-ral

Description: The definiens of df-ral , A. x ( x e. A -> ph ) 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 ph holds for all elements of A . To this end, x must not be free in A , though . Should instead A vary with x , then we rather focus on those x , that happen to be an element of their respective A ( x ) . 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 y , disjoint from all other variables, to describe an element in A . It lets x appear as a formal parameter with no connection to A , but occurrences in ph are still honored.

The resulting subexpression A. x ( x = y -> ph ) is [ y / x ] ph in disguise (see wl-dfralsb ).

If x is not free in A , a simplification is possible ( see wl-dfralf , wl-dfralv ). (Contributed by NM, 19-Aug-1993) Isolate x from A , idea of Mario Carneiro. (Revised by Wolf Lammen, 21-May-2023)

	Ref	Expression
Assertion	df-wl-ral	$$⊢\forall x:A\phi \leftrightarrow \forall y\left(y\in A\to \forall x\left(x=y\to \phi \right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3	2 0 1	wl-ral	$$wff\forall x:A\phi$$
4		vy	$$setvary$$
5	4	cv	$$setvary$$
6	5 1	wcel	$$wffy\in A$$
7	0	cv	$$setvarx$$
8	7 5	wceq	$$wffx=y$$
9	8 2	wi	$$wff\left(x=y\to \phi \right)$$
10	9 0	wal	$$wff\forall x\left(x=y\to \phi \right)$$
11	6 10	wi	$$wff\left(y\in A\to \forall x\left(x=y\to \phi \right)\right)$$
12	11 4	wal	$$wff\forall y\left(y\in A\to \forall x\left(x=y\to \phi \right)\right)$$
13	3 12	wb	$$wff\left(\forall x:A\phi \leftrightarrow \forall y\left(y\in A\to \forall x\left(x=y\to \phi \right)\right)\right)$$