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

Metamath Proof Explorer

Theorem sbralieALT

Description: Alternative shorter proof of sbralie dependent on ax-ext , df-cleq , df-clel . (Contributed by NM, 5-Sep-2004) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis sbralie.1 
|- ( x = y -> ( ph <-> ps ) )
Assertion sbralieALT 
|- ( 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 cbvralsvw 
 |-  ( A. y e. x ps <-> A. z e. x [ z / y ] ps )
3 2 sbbii 
 |-  ( [ y / x ] A. y e. x ps <-> [ y / x ] A. z e. x [ z / y ] ps )
4 raleq 
 |-  ( x = y -> ( A. z e. x [ z / y ] ps <-> A. z e. y [ z / y ] ps ) )
5 4 sbievw 
 |-  ( [ y / x ] A. z e. x [ z / y ] ps <-> A. z e. y [ z / y ] ps )
6 cbvralsvw 
 |-  ( A. z e. y [ z / y ] ps <-> A. x e. y [ x / z ] [ z / y ] ps )
7 sbco2vv 
 |-  ( [ x / z ] [ z / y ] ps <-> [ x / y ] ps )
8 1 bicomd 
 |-  ( x = y -> ( ps <-> ph ) )
9 8 equcoms 
 |-  ( y = x -> ( ps <-> ph ) )
10 9 sbievw 
 |-  ( [ x / y ] ps <-> ph )
11 7 10 bitri 
 |-  ( [ x / z ] [ z / y ] ps <-> ph )
12 11 ralbii 
 |-  ( A. x e. y [ x / z ] [ z / y ] ps <-> A. x e. y ph )
13 6 12 bitri 
 |-  ( A. z e. y [ z / y ] ps <-> A. x e. y ph )
14 3 5 13 3bitrri 
 |-  ( A. x e. y ph <-> [ y / x ] A. y e. x ps )