Metamath Proof Explorer

Theorem spimfv

Description: Specialization, using implicit substitution. Version of spim with a disjoint variable condition, which does not require ax-13 . See spimvw for a version with two disjoint variable conditions, requiring fewer axioms, and spimv for another variant. (Contributed by NM, 10-Jan-1993) (Revised by BJ, 31-May-2019)

Ref Expression
Hypotheses x ψ
spimfv.1 x = y φ ψ
Assertion spimfv x φ ψ


Step Hyp Ref Expression
1 x ψ
2 spimfv.1 x = y φ ψ
3 ax6ev x x = y
4 3 2 eximii x φ ψ
5 1 4 19.36i x φ ψ