This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( [ t / x ] ph <-> ph )

Proof

Step Hyp Ref Expression
1 spsbe 
 |-  ( [ t / x ] ph -> E. x ph )
2 ax5e 
 |-  ( E. x ph -> ph )
3 1 2 syl 
 |-  ( [ t / x ] ph -> ph )
4 ax-5 
 |-  ( ph -> A. x ph )
5 stdpc4 
 |-  ( A. x ph -> [ t / x ] ph )
6 4 5 syl 
 |-  ( ph -> [ t / x ] ph )
7 3 6 impbii 
 |-  ( [ t / x ] ph <-> ph )