This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998) Drop ax-10 , ax-11 , ax-12 . (Revised by SN, 12-Dec-2023)
|
|
Ref |
Expression |
|
Hypothesis |
rspcv.1 |
|- ( x = A -> ( ph <-> ps ) ) |
|
Assertion |
rspcv |
|- ( A e. B -> ( A. x e. B ph -> ps ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rspcv.1 |
|- ( x = A -> ( ph <-> ps ) ) |
| 2 |
|
id |
|- ( A e. B -> A e. B ) |
| 3 |
1
|
adantl |
|- ( ( A e. B /\ x = A ) -> ( ph <-> ps ) ) |
| 4 |
2 3
|
rspcdv |
|- ( A e. B -> ( A. x e. B ph -> ps ) ) |