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\in \mathrm{V}$$
	spsbcdi.2	$$⊢\phi \to \forall x\chi$$
	spsbcdi.3	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi \leftrightarrow \psi$$
Assertion	spsbcdi	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		spsbcdi.1	$$⊢A\in \mathrm{V}$$
2		spsbcdi.2	$$⊢\phi \to \forall x\chi$$
3		spsbcdi.3	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi \leftrightarrow \psi$$
4	1	a1i	$$⊢\phi \to A\in \mathrm{V}$$
5	4 2	spsbcd	$$⊢\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi$$
6	5 3	sylib	$$⊢\phi \to \psi$$