Metamath Proof Explorer

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 . (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 sbim 
 |-  ( [ y / z ] ( x e. z -> ph ) <-> ( [ y / z ] x e. z -> [ y / z ] ph ) )
4 elsb2 
 |-  ( [ y / z ] x e. z <-> x e. y )
5 sbv 
 |-  ( [ y / z ] ph <-> ph )
6 4 5 imbi12i 
 |-  ( ( [ y / z ] x e. z -> [ y / z ] ph ) <-> ( x e. y -> ph ) )
7 3 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 sbim 
 |-  ( [ z / x ] ( y e. x -> ps ) <-> ( [ z / x ] y e. x -> [ z / x ] ps ) )
16 elsb2 
 |-  ( [ z / x ] y e. x <-> y e. z )
17 sbv 
 |-  ( [ z / x ] ps <-> ps )
18 16 17 imbi12i 
 |-  ( ( [ z / x ] y e. x -> [ z / x ] ps ) <-> ( y e. z -> ps ) )
19 15 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 )