Description: Obsolete version of rspcv as of 12-Dec-2023. Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | rspcv.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
| Assertion | rspcvOLD | |- ( A e. B -> ( A. x e. B ph -> ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rspcv.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
| 2 | nfv | |- F/ x ps |
|
| 3 | 2 1 | rspc | |- ( A e. B -> ( A. x e. B ph -> ps ) ) |