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 xψ
rspcegf.2 _xA
rspcegf.3 _xB
rspcegf.4 x=Aφψ
Assertion rspcegf ABψxBφ

Proof

Step Hyp Ref Expression
1 rspcegf.1 xψ
2 rspcegf.2 _xA
3 rspcegf.3 _xB
4 rspcegf.4 x=Aφψ
5 2 3 nfel xAB
6 5 1 nfan xABψ
7 eleq1 x=AxBAB
8 7 4 anbi12d x=AxBφABψ
9 2 6 8 spcegf ABABψxxBφ
10 9 anabsi5 ABψxxBφ
11 df-rex xBφxxBφ
12 10 11 sylibr ABψxBφ