Metamath Proof Explorer


Theorem sbv

Description: Substitution for a variable not occurring in a proposition. See sbf for a version without disjoint variable condition on x , ph . If one adds a disjoint variable condition on x , t , then sbv can be proved directly by chaining equsv with sb6 . (Contributed by BJ, 22-Dec-2020)

Ref Expression
Assertion sbv txφφ

Proof

Step Hyp Ref Expression
1 spsbe txφxφ
2 ax5e xφφ
3 1 2 syl txφφ
4 ax-5 φxφ
5 stdpc4 xφtxφ
6 4 5 syl φtxφ
7 3 6 impbii txφφ