Definition df-ral

Description: Define restricted universal quantification. Special case of Definition 4.15(3) of TakeutiZaring p. 22.

Note: This notation is most often used to express that ph holds for all elements of a given class A . For this reading F/_ x A is required, though, for example, asserted when x and A are disjoint.

Should instead A depend on x , you rather focus on those x that happen to be contained in the corresponding A ( x ) . This hardly used interpretation could still occur naturally. For some examples, look at ralndv1 or ralndv2 , courtesy of AV.

So be careful to either keep A independent of x , or adjust your comments to include such exotic cases. (Contributed by NM, 19-Aug-1993)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		wph	$$wff\phi$$
3	2 0 1	wral	$$wff\forall x\in A\phi$$
4	0	cv	$$setvarx$$
5	4 1	wcel	$$wffx\in A$$
6	5 2	wi	$$wff\left(x\in A\to \phi \right)$$
7	6 0	wal	$$wff\forall x\left(x\in A\to \phi \right)$$
8	3 7	wb	$$wff\left(\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)\right)$$