# Metamath Proof Explorer

## 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
`|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )`

### Detailed syntax breakdown

Step Hyp Ref Expression
0 vx
` |-  x`
1 cA
` |-  A`
2 wph
` |-  ph`
3 2 0 1 wral
` |-  A. x e. A ph`
4 0 cv
` |-  x`
5 4 1 wcel
` |-  x e. A`
6 5 2 wi
` |-  ( x e. A -> ph )`
7 6 0 wal
` |-  A. x ( x e. A -> ph )`
8 3 7 wb
` |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )`