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

Metamath Proof Explorer

Theorem rspce

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998) (Revised by Mario Carneiro, 11-Oct-2016)

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

Proof

Step Hyp Ref Expression
1 rspc.1 
 |-  F/ x ps
2 rspc.2 
 |-  ( x = A -> ( ph <-> ps ) )
3 nfcv 
 |-  F/_ x A
4 nfv 
 |-  F/ x A e. B
5 4 1 nfan 
 |-  F/ x ( A e. B /\ ps )
6 eleq1 
 |-  ( x = A -> ( x e. B <-> A e. B ) )
7 6 2 anbi12d 
 |-  ( x = A -> ( ( x e. B /\ ph ) <-> ( A e. B /\ ps ) ) )
8 3 5 7 spcegf 
 |-  ( A e. B -> ( ( A e. B /\ ps ) -> E. x ( x e. B /\ ph ) ) )
9 8 anabsi5 
 |-  ( ( A e. B /\ ps ) -> E. x ( x e. B /\ ph ) )
10 df-rex 
 |-  ( E. x e. B ph <-> E. x ( x e. B /\ ph ) )
11 9 10 sylibr 
 |-  ( ( A e. B /\ ps ) -> E. x e. B ph )