Theorem sbralie

Description: Implicit to explicit substitution that swaps variables in a rectrictedly universally quantified expression. (Contributed by NM, 5-Sep-2004) Avoid ax-ext , df-cleq , df-clel . (Revised by Wolf Lammen, 10-Mar-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		nfv	|- F/ z ph
4	3	sblim	|- ( [ y / z ] ( x e. z -> ph ) <-> ( [ y / z ] x e. z -> ph ) )
5		elsb2	|- ( [ y / z ] x e. z <-> x e. y )
6	5	imbi1i	|- ( ( [ y / z ] x e. z -> ph ) <-> ( x e. y -> ph ) )
7	4 6	bitri	|- ( [ y / z ] ( x e. z -> ph ) <-> ( x e. y -> ph ) )
8	7	albii	|- ( A. x [ y / z ] ( x e. z -> ph ) <-> A. x ( x e. y -> ph ) )
9		elequ1	|- ( x = y -> ( x e. z <-> y e. z ) )
10	9 1	imbi12d	|- ( x = y -> ( ( x e. z -> ph ) <-> ( y e. z -> ps ) ) )
11	10	cbvalvw	|- ( A. x ( x e. z -> ph ) <-> A. y ( y e. z -> ps ) )
12		df-ral	|- ( A. y e. x ps <-> A. y ( y e. x -> ps ) )
13	12	sbbii	|- ( [ z / x ] A. y e. x ps <-> [ z / x ] A. y ( y e. x -> ps ) )
14		sbal	|- ( [ z / x ] A. y ( y e. x -> ps ) <-> A. y [ z / x ] ( y e. x -> ps ) )
15		nfv	|- F/ x ps
16	15	sblim	|- ( [ z / x ] ( y e. x -> ps ) <-> ( [ z / x ] y e. x -> ps ) )
17		elsb2	|- ( [ z / x ] y e. x <-> y e. z )
18	17	imbi1i	|- ( ( [ z / x ] y e. x -> ps ) <-> ( y e. z -> ps ) )
19	16 18	bitri	|- ( [ z / x ] ( y e. x -> ps ) <-> ( y e. z -> ps ) )
20	19	albii	|- ( A. y [ z / x ] ( y e. x -> ps ) <-> A. y ( y e. z -> ps ) )
21	13 14 20	3bitrri	|- ( A. y ( y e. z -> ps ) <-> [ z / x ] A. y e. x ps )
22	11 21	bitri	|- ( A. x ( x e. z -> ph ) <-> [ z / x ] A. y e. x ps )
23	22	sbbii	|- ( [ y / z ] A. x ( x e. z -> ph ) <-> [ y / z ] [ z / x ] A. y e. x ps )
24		sbal	|- ( [ y / z ] A. x ( x e. z -> ph ) <-> A. x [ y / z ] ( x e. z -> ph ) )
25		sbco2vv	|- ( [ y / z ] [ z / x ] A. y e. x ps <-> [ y / x ] A. y e. x ps )
26	23 24 25	3bitr3i	|- ( A. x [ y / z ] ( x e. z -> ph ) <-> [ y / x ] A. y e. x ps )
27	2 8 26	3bitr2i	|- ( A. x e. y ph <-> [ y / x ] A. y e. x ps )