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 )