Theorem axextdfeq

Description: A version of ax-ext for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010)

	Ref	Expression
Assertion	axextdfeq	|- E. z ( ( z e. x -> z e. y ) -> ( ( z e. y -> z e. x ) -> ( x e. w -> y e. w ) ) )

Proof

Step	Hyp	Ref	Expression
1		axextnd	|- E. z ( ( z e. x <-> z e. y ) -> x = y )
2		ax8	|- ( x = y -> ( x e. w -> y e. w ) )
3	2	imim2i	|- ( ( ( z e. x <-> z e. y ) -> x = y ) -> ( ( z e. x <-> z e. y ) -> ( x e. w -> y e. w ) ) )
4	1 3	eximii	|- E. z ( ( z e. x <-> z e. y ) -> ( x e. w -> y e. w ) )
5		biimpexp	|- ( ( ( z e. x <-> z e. y ) -> ( x e. w -> y e. w ) ) <-> ( ( z e. x -> z e. y ) -> ( ( z e. y -> z e. x ) -> ( x e. w -> y e. w ) ) ) )
6	5	exbii	|- ( E. z ( ( z e. x <-> z e. y ) -> ( x e. w -> y e. w ) ) <-> E. z ( ( z e. x -> z e. y ) -> ( ( z e. y -> z e. x ) -> ( x e. w -> y e. w ) ) ) )
7	4 6	mpbi	|- E. z ( ( z e. x -> z e. y ) -> ( ( z e. y -> z e. x ) -> ( x e. w -> y e. w ) ) )