Metamath Proof Explorer

Theorem wl-sb8eutv

Description: Substitution of variable in universal quantifier. Closed form of sb8euv . (Contributed by Wolf Lammen, 3-May-2025)

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

Proof

Step Hyp Ref Expression
1 nfnf1 
 |-  F/ y F/ y ph
2 1 nfal 
 |-  F/ y A. x F/ y ph
3 equsb3 
 |-  ( [ v / x ] x = u <-> v = u )
4 3 sblbis 
 |-  ( [ v / x ] ( ph <-> x = u ) <-> ( [ v / x ] ph <-> v = u ) )
5 wl-nfsbtv 
 |-  ( A. x F/ y ph -> F/ y [ v / x ] ph )
6 nfvd 
 |-  ( A. x F/ y ph -> F/ y v = u )
7 5 6 nfbid 
 |-  ( A. x F/ y ph -> F/ y ( [ v / x ] ph <-> v = u ) )
8 4 7 nfxfrd 
 |-  ( A. x F/ y ph -> F/ y [ v / x ] ( ph <-> x = u ) )
9 sbequ 
 |-  ( v = y -> ( [ v / x ] ( ph <-> x = u ) <-> [ y / x ] ( ph <-> x = u ) ) )
10 9 a1i 
 |-  ( A. x F/ y ph -> ( v = y -> ( [ v / x ] ( ph <-> x = u ) <-> [ y / x ] ( ph <-> x = u ) ) ) )
11 2 8 10 cbvaldw 
 |-  ( A. x F/ y ph -> ( A. v [ v / x ] ( ph <-> x = u ) <-> A. y [ y / x ] ( ph <-> x = u ) ) )
12 sb8v 
 |-  ( A. x ( ph <-> x = u ) <-> A. v [ v / x ] ( ph <-> x = u ) )
13 12 bicomi 
 |-  ( A. v [ v / x ] ( ph <-> x = u ) <-> A. x ( ph <-> x = u ) )
14 equsb3 
 |-  ( [ y / x ] x = u <-> y = u )
15 14 sblbis 
 |-  ( [ y / x ] ( ph <-> x = u ) <-> ( [ y / x ] ph <-> y = u ) )
16 15 albii 
 |-  ( A. y [ y / x ] ( ph <-> x = u ) <-> A. y ( [ y / x ] ph <-> y = u ) )
17 11 13 16 3bitr3g 
 |-  ( A. x F/ y ph -> ( A. x ( ph <-> x = u ) <-> A. y ( [ y / x ] ph <-> y = u ) ) )
18 17 exbidv 
 |-  ( A. x F/ y ph -> ( E. u A. x ( ph <-> x = u ) <-> E. u A. y ( [ y / x ] ph <-> y = u ) ) )
19 eu6 
 |-  ( E! x ph <-> E. u A. x ( ph <-> x = u ) )
20 eu6 
 |-  ( E! y [ y / x ] ph <-> E. u A. y ( [ y / x ] ph <-> y = u ) )
21 18 19 20 3bitr4g 
 |-  ( A. x F/ y ph -> ( E! x ph <-> E! y [ y / x ] ph ) )