Metamath Proof Explorer

Theorem wl-sb8mot

Description: Substitution of variable in universal quantifier. Closed form of sb8mo . (Contributed by Wolf Lammen, 11-Aug-2019)

Ref Expression
Assertion wl-sb8mot 
|- ( A. x F/ y ph -> ( E* x ph <-> E* y [ y / x ] ph ) )

Proof

Step Hyp Ref Expression
1 wl-sb8et 
 |-  ( A. x F/ y ph -> ( E. x ph <-> E. y [ y / x ] ph ) )
2 wl-sb8eut 
 |-  ( A. x F/ y ph -> ( E! x ph <-> E! y [ y / x ] ph ) )
3 1 2 imbi12d 
 |-  ( A. x F/ y ph -> ( ( E. x ph -> E! x ph ) <-> ( E. y [ y / x ] ph -> E! y [ y / x ] ph ) ) )
4 moeu 
 |-  ( E* x ph <-> ( E. x ph -> E! x ph ) )
5 moeu 
 |-  ( E* y [ y / x ] ph <-> ( E. y [ y / x ] ph -> E! y [ y / x ] ph ) )
6 3 4 5 3bitr4g 
 |-  ( A. x F/ y ph -> ( E* x ph <-> E* y [ y / x ] ph ) )