This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )