This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspc

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005) (Revised by Mario Carneiro, 11-Oct-2016)

Ref Expression
Hypotheses rspc.1 
|- F/ x ps
rspc.2 
|- ( x = A -> ( ph <-> ps ) )
Assertion rspc 
|- ( A e. B -> ( A. x e. B ph -> ps ) )

Proof

Step Hyp Ref Expression
1 rspc.1 
 |-  F/ x ps
2 rspc.2 
 |-  ( x = A -> ( ph <-> ps ) )
3 df-ral 
 |-  ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
4 nfcv 
 |-  F/_ x A
5 nfv 
 |-  F/ x A e. B
6 5 1 nfim 
 |-  F/ x ( A e. B -> ps )
7 eleq1 
 |-  ( x = A -> ( x e. B <-> A e. B ) )
8 7 2 imbi12d 
 |-  ( x = A -> ( ( x e. B -> ph ) <-> ( A e. B -> ps ) ) )
9 4 6 8 spcgf 
 |-  ( A e. B -> ( A. x ( x e. B -> ph ) -> ( A e. B -> ps ) ) )
10 9 pm2.43a 
 |-  ( A e. B -> ( A. x ( x e. B -> ph ) -> ps ) )
11 3 10 biimtrid 
 |-  ( A e. B -> ( A. x e. B ph -> ps ) )