Metamath Proof Explorer


Theorem sb8mo

Description: Variable substitution for the at-most-one quantifier. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Alexander van der Vekens, 17-Jun-2017) (New usage is discouraged.)

Ref Expression
Hypothesis sb8eu.1
|- F/ y ph
Assertion sb8mo
|- ( E* x ph <-> E* y [ y / x ] ph )

Proof

Step Hyp Ref Expression
1 sb8eu.1
 |-  F/ y ph
2 1 sb8e
 |-  ( E. x ph <-> E. y [ y / x ] ph )
3 1 sb8eu
 |-  ( E! x ph <-> E! y [ y / x ] ph )
4 2 3 imbi12i
 |-  ( ( E. x ph -> E! x ph ) <-> ( E. y [ y / x ] ph -> E! y [ y / x ] ph ) )
5 moeu
 |-  ( E* x ph <-> ( E. x ph -> E! x ph ) )
6 moeu
 |-  ( E* y [ y / x ] ph <-> ( E. y [ y / x ] ph -> E! y [ y / x ] ph ) )
7 4 5 6 3bitr4i
 |-  ( E* x ph <-> E* y [ y / x ] ph )