Theorem axextndbi

Description: axextnd as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010)

	Ref	Expression
Assertion	axextndbi	|- E. z ( x = y <-> ( z e. x <-> z e. y ) )

Proof

Step	Hyp	Ref	Expression
1		axextnd	|- E. z ( ( z e. x <-> z e. y ) -> x = y )
2		elequ2	|- ( x = y -> ( z e. x <-> z e. y ) )
3	2	jctl	|- ( ( ( z e. x <-> z e. y ) -> x = y ) -> ( ( x = y -> ( z e. x <-> z e. y ) ) /\ ( ( z e. x <-> z e. y ) -> x = y ) ) )
4	1 3	eximii	|- E. z ( ( x = y -> ( z e. x <-> z e. y ) ) /\ ( ( z e. x <-> z e. y ) -> x = y ) )
5		dfbi2	|- ( ( x = y <-> ( z e. x <-> z e. y ) ) <-> ( ( x = y -> ( z e. x <-> z e. y ) ) /\ ( ( z e. x <-> z e. y ) -> x = y ) ) )
6	5	exbii	|- ( E. z ( x = y <-> ( z e. x <-> z e. y ) ) <-> E. z ( ( x = y -> ( z e. x <-> z e. y ) ) /\ ( ( z e. x <-> z e. y ) -> x = y ) ) )
7	4 6	mpbir	|- E. z ( x = y <-> ( z e. x <-> z e. y ) )