Theorem spsbcdi

Description: A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019)

	Ref	Expression
Hypotheses	spsbcdi.1	|- A e. _V
	spsbcdi.2	|- ( ph -> A. x ch )
	spsbcdi.3	|- ( [. A / x ]. ch <-> ps )
Assertion	spsbcdi	|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		spsbcdi.1	|- A e. _V
2		spsbcdi.2	|- ( ph -> A. x ch )
3		spsbcdi.3	|- ( [. A / x ]. ch <-> ps )
4	1	a1i	|- ( ph -> A e. _V )
5	4 2	spsbcd	|- ( ph -> [. A / x ]. ch )
6	5 3	sylib	|- ( ph -> ps )