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

Metamath Proof Explorer

Theorem sbralieOLD

Description: Obsolete version of sbralie as of 13-Nov-2025. (Contributed by NM, 5-Sep-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis sbralie.1 
|- ( x = y -> ( ph <-> ps ) )
Assertion sbralieOLD 
|- ( 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 )