Description: Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | rspa | ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rsp | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) | |
2 | 1 | imp | ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 ) |