Metamath Proof Explorer


Theorem spcimegf

Description: Existential specialization, using implicit substitution. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses spcimgf.1 _xA
spcimgf.2 xψ
spcimegf.3 x=Aψφ
Assertion spcimegf AVψxφ

Proof

Step Hyp Ref Expression
1 spcimgf.1 _xA
2 spcimgf.2 xψ
3 spcimegf.3 x=Aψφ
4 2 nfn x¬ψ
5 3 con3d x=A¬φ¬ψ
6 1 4 5 spcimgf AVx¬φ¬ψ
7 6 con2d AVψ¬x¬φ
8 df-ex xφ¬x¬φ
9 7 8 syl6ibr AVψxφ