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	⊢ 𝐴 ∈ V
	spsbcdi.2	⊢ ( 𝜑 → ∀ 𝑥 𝜒 )
	spsbcdi.3	⊢ ( [ 𝐴 / 𝑥 ] 𝜒 ↔ 𝜓 )
Assertion	spsbcdi	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		spsbcdi.1	⊢ 𝐴 ∈ V
2		spsbcdi.2	⊢ ( 𝜑 → ∀ 𝑥 𝜒 )
3		spsbcdi.3	⊢ ( [ 𝐴 / 𝑥 ] 𝜒 ↔ 𝜓 )
4	1	a1i	⊢ ( 𝜑 → 𝐴 ∈ V )
5	4 2	spsbcd	⊢ ( 𝜑 → [ 𝐴 / 𝑥 ] 𝜒 )
6	5 3	sylib	⊢ ( 𝜑 → 𝜓 )