Metamath Proof Explorer

Theorem sbmo

Description: Substitution into an at-most-one quantifier. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion sbmo 
|- ( [ y / x ] E* z ph <-> E* z [ y / x ] ph )

Proof

Step Hyp Ref Expression
1 sbex 
 |-  ( [ y / x ] E. w A. z ( ph -> z = w ) <-> E. w [ y / x ] A. z ( ph -> z = w ) )
2 nfv 
 |-  F/ x z = w
3 2 sblim 
 |-  ( [ y / x ] ( ph -> z = w ) <-> ( [ y / x ] ph -> z = w ) )
4 3 sbalv 
 |-  ( [ y / x ] A. z ( ph -> z = w ) <-> A. z ( [ y / x ] ph -> z = w ) )
5 4 exbii 
 |-  ( E. w [ y / x ] A. z ( ph -> z = w ) <-> E. w A. z ( [ y / x ] ph -> z = w ) )
6 1 5 bitri 
 |-  ( [ y / x ] E. w A. z ( ph -> z = w ) <-> E. w A. z ( [ y / x ] ph -> z = w ) )
7 df-mo 
 |-  ( E* z ph <-> E. w A. z ( ph -> z = w ) )
8 7 sbbii 
 |-  ( [ y / x ] E* z ph <-> [ y / x ] E. w A. z ( ph -> z = w ) )
9 df-mo 
 |-  ( E* z [ y / x ] ph <-> E. w A. z ( [ y / x ] ph -> z = w ) )
10 6 8 9 3bitr4i 
 |-  ( [ y / x ] E* z ph <-> E* z [ y / x ] ph )