Metamath Proof Explorer

Theorem wl-sb8eft

Description: Substitution of variable in existentialal quantifier. Closed form of sb8ef . (Contributed by Wolf Lammen, 27-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 nfnt 
 |-  ( F/ y ph -> F/ y -. ph )
2 1 alimi 
 |-  ( A. x F/ y ph -> A. x F/ y -. ph )
3 wl-sb8ft 
 |-  ( A. x F/ y -. ph -> ( A. x -. ph <-> A. y [ y / x ] -. ph ) )
4 2 3 syl 
 |-  ( 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 ) )