Metamath Proof Explorer


Theorem speivw

Description: Version of spei with a disjoint variable condition, which does not require ax-13 (neither ax-7 nor ax-12 ). (Contributed by BJ, 31-May-2019)

Ref Expression
Hypotheses speivw.1 x=yφψ
speivw.2 ψ
Assertion speivw xφ

Proof

Step Hyp Ref Expression
1 speivw.1 x=yφψ
2 speivw.2 ψ
3 1 biimprd x=yψφ
4 3 2 speiv xφ