**Description:** Restricted specialization. (Contributed by NM, 17-Oct-1996)

Ref | Expression | ||
---|---|---|---|

Assertion | rsp | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | df-ral | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) | |

2 | sp | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) | |

3 | 1 2 | sylbi | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |