Metamath Proof Explorer


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 ( 𝜑𝜓 )