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 | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | cA | ⊢ 𝐴 | |
| 2 | wph | ⊢ 𝜑 | |
| 3 | 2 0 1 | wral | ⊢ ∀ 𝑥 ∈ 𝐴 𝜑 |
| 4 | 0 | cv | ⊢ 𝑥 |
| 5 | 4 1 | wcel | ⊢ 𝑥 ∈ 𝐴 |
| 6 | 5 2 | wi | ⊢ ( 𝑥 ∈ 𝐴 → 𝜑 ) |
| 7 | 6 0 | wal | ⊢ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) |
| 8 | 3 7 | wb | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |