Metamath Proof Explorer


Theorem rsp

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

Ref Expression
Assertion rsp x A φ x A φ

Proof

Step Hyp Ref Expression
1 df-ral x A φ x x A φ
2 sp x x A φ x A φ
3 1 2 sylbi x A φ x A φ