Theorem sbralie

Description: Implicit to explicit substitution that swaps variables in a restrictedly universally quantified expression. (Contributed by NM, 5-Sep-2004) Avoid ax-ext , df-cleq , df-clel . (Revised by Wolf Lammen, 10-Mar-2025) Avoid ax-10 , ax-12 . (Revised by SN, 13-Nov-2025)

	Ref	Expression
Hypothesis	sbralie.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	sbralie	|- ( A. x e. y ph <-> [ y / x ] A. y e. x ps )

Proof

Step	Hyp	Ref	Expression
1		sbralie.1	|- ( x = y -> ( ph <-> ps ) )
2		df-ral	|- ( A. x e. y ph <-> A. x ( x e. y -> ph ) )
3		elequ2	|- ( z = y -> ( x e. z <-> x e. y ) )
4	3	imbi1d	|- ( z = y -> ( ( x e. z -> ph ) <-> ( x e. y -> ph ) ) )
5	4	sbievw	|- ( [ y / z ] ( x e. z -> ph ) <-> ( x e. y -> ph ) )
6	5	albii	|- ( A. x [ y / z ] ( x e. z -> ph ) <-> A. x ( x e. y -> ph ) )
7		elequ1	|- ( x = y -> ( x e. z <-> y e. z ) )
8	7 1	imbi12d	|- ( x = y -> ( ( x e. z -> ph ) <-> ( y e. z -> ps ) ) )
9	8	cbvalvw	|- ( A. x ( x e. z -> ph ) <-> A. y ( y e. z -> ps ) )
10		df-ral	|- ( A. y e. x ps <-> A. y ( y e. x -> ps ) )
11	10	sbbii	|- ( [ z / x ] A. y e. x ps <-> [ z / x ] A. y ( y e. x -> ps ) )
12		sbal	|- ( [ z / x ] A. y ( y e. x -> ps ) <-> A. y [ z / x ] ( y e. x -> ps ) )
13		elequ2	|- ( x = z -> ( y e. x <-> y e. z ) )
14	13	imbi1d	|- ( x = z -> ( ( y e. x -> ps ) <-> ( y e. z -> ps ) ) )
15	14	sbievw	|- ( [ z / x ] ( y e. x -> ps ) <-> ( y e. z -> ps ) )
16	15	albii	|- ( A. y [ z / x ] ( y e. x -> ps ) <-> A. y ( y e. z -> ps ) )
17	11 12 16	3bitrri	|- ( A. y ( y e. z -> ps ) <-> [ z / x ] A. y e. x ps )
18	9 17	bitri	|- ( A. x ( x e. z -> ph ) <-> [ z / x ] A. y e. x ps )
19	18	sbbii	|- ( [ y / z ] A. x ( x e. z -> ph ) <-> [ y / z ] [ z / x ] A. y e. x ps )
20		sbal	|- ( [ y / z ] A. x ( x e. z -> ph ) <-> A. x [ y / z ] ( x e. z -> ph ) )
21		sbco2vv	|- ( [ y / z ] [ z / x ] A. y e. x ps <-> [ y / x ] A. y e. x ps )
22	19 20 21	3bitr3i	|- ( A. x [ y / z ] ( x e. z -> ph ) <-> [ y / x ] A. y e. x ps )
23	2 6 22	3bitr2i	|- ( A. x e. y ph <-> [ y / x ] A. y e. x ps )