This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvsbvf

Description: Change the bound variable (i.e. the substituted one) in wff's linked by implicit substitution. The proof was part of a former cbvabw version. (Contributed by GG and WL, 26-Oct-2024)

Ref Expression
Hypotheses cbvsbvf.1 
|- F/ y ph
cbvsbvf.2 
|- F/ x ps
cbvsbvf.3 
|- ( x = y -> ( ph <-> ps ) )
Assertion cbvsbvf 
|- ( [ z / x ] ph <-> [ z / y ] ps )

Proof

Step Hyp Ref Expression
1 cbvsbvf.1 
 |-  F/ y ph
2 cbvsbvf.2 
 |-  F/ x ps
3 cbvsbvf.3 
 |-  ( x = y -> ( ph <-> ps ) )
4 nfv 
 |-  F/ y x = w
5 4 1 nfim 
 |-  F/ y ( x = w -> ph )
6 nfv 
 |-  F/ x y = w
7 6 2 nfim 
 |-  F/ x ( y = w -> ps )
8 equequ1 
 |-  ( x = y -> ( x = w <-> y = w ) )
9 8 3 imbi12d 
 |-  ( x = y -> ( ( x = w -> ph ) <-> ( y = w -> ps ) ) )
10 5 7 9 cbvalv1 
 |-  ( A. x ( x = w -> ph ) <-> A. y ( y = w -> ps ) )
11 10 imbi2i 
 |-  ( ( w = z -> A. x ( x = w -> ph ) ) <-> ( w = z -> A. y ( y = w -> ps ) ) )
12 11 albii 
 |-  ( A. w ( w = z -> A. x ( x = w -> ph ) ) <-> A. w ( w = z -> A. y ( y = w -> ps ) ) )
13 dfsb 
 |-  ( [ z / x ] ph <-> A. w ( w = z -> A. x ( x = w -> ph ) ) )
14 dfsb 
 |-  ( [ z / y ] ps <-> A. w ( w = z -> A. y ( y = w -> ps ) ) )
15 12 13 14 3bitr4i 
 |-  ( [ z / x ] ph <-> [ z / y ] ps )