Metamath Proof Explorer

Theorem wl-sb8et

Description: Substitution of variable in universal quantifier. Closed form of sb8e . (Contributed by Wolf Lammen, 27-Jul-2019)

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

Proof

Step Hyp Ref Expression
1 nfnbi 
 |-  ( F/ y ph <-> F/ y -. ph )
2 1 albii 
 |-  ( A. x F/ y ph <-> A. x F/ y -. ph )
3 wl-sb8t 
 |-  ( A. x F/ y -. ph -> ( A. x -. ph <-> A. y [ y / x ] -. ph ) )
4 2 3 sylbi 
 |-  ( A. x F/ y ph -> ( A. x -. ph <-> A. y [ y / x ] -. ph ) )
5 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
6 sbn 
 |-  ( [ y / x ] -. ph <-> -. [ y / x ] ph )
7 6 albii 
 |-  ( A. y [ y / x ] -. ph <-> A. y -. [ y / x ] ph )
8 alnex 
 |-  ( A. y -. [ y / x ] ph <-> -. E. y [ y / x ] ph )
9 7 8 bitri 
 |-  ( A. y [ y / x ] -. ph <-> -. E. y [ y / x ] ph )
10 4 5 9 3bitr3g 
 |-  ( A. x F/ y ph -> ( -. E. x ph <-> -. E. y [ y / x ] ph ) )
11 10 con4bid 
 |-  ( A. x F/ y ph -> ( E. x ph <-> E. y [ y / x ] ph ) )