Theorem sbbib

Description: Reversal of substitution. (Contributed by AV, 6-Aug-2023) (Proof shortened by Wolf Lammen, 4-Sep-2023)

	Ref	Expression
Hypotheses	sbbib.y	|- F/ y ph
	sbbib.x	|- F/ x ps
Assertion	sbbib	|- ( A. y ( [ y / x ] ph <-> ps ) <-> A. x ( ph <-> [ x / y ] ps ) )

Proof

Step	Hyp	Ref	Expression
1		sbbib.y	|- F/ y ph
2		sbbib.x	|- F/ x ps
3		nfs1v	|- F/ x [ y / x ] ph
4	3 2	nfbi	|- F/ x ( [ y / x ] ph <-> ps )
5		nfs1v	|- F/ y [ x / y ] ps
6	1 5	nfbi	|- F/ y ( ph <-> [ x / y ] ps )
7		sbequ12r	|- ( y = x -> ( [ y / x ] ph <-> ph ) )
8		sbequ12	|- ( y = x -> ( ps <-> [ x / y ] ps ) )
9	7 8	bibi12d	|- ( y = x -> ( ( [ y / x ] ph <-> ps ) <-> ( ph <-> [ x / y ] ps ) ) )
10	4 6 9	cbvalv1	|- ( A. y ( [ y / x ] ph <-> ps ) <-> A. x ( ph <-> [ x / y ] ps ) )