Theorem sbievg

Description: Substitution applied to expressions linked by implicit substitution. The proof was part of a former cbvabw version. (Contributed by GG and WL, 26-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sbievg.1	|- F/ y ph
2		sbievg.2	|- F/ x ps
3		sbievg.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		df-sb	|- ( [ z / x ] ph <-> A. w ( w = z -> A. x ( x = w -> ph ) ) )
14		df-sb	|- ( [ z / y ] ps <-> A. w ( w = z -> A. y ( y = w -> ps ) ) )
15	12 13 14	3bitr4i	|- ( [ z / x ] ph <-> [ z / y ] ps )