Metamath Proof Explorer


Theorem spcegv

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994) Avoid ax-10 , ax-11 . (Revised by Wolf Lammen, 25-Aug-2023)

Ref Expression
Hypothesis spcgv.1 x=Aφψ
Assertion spcegv AVψxφ

Proof

Step Hyp Ref Expression
1 spcgv.1 x=Aφψ
2 elisset AVxx=A
3 1 biimprcd ψx=Aφ
4 3 eximdv ψxx=Axφ
5 2 4 syl5com AVψxφ