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

Metamath Proof Explorer

Theorem rspcegf

Description: A version of rspcev using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Proof

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