Theorem axextdist

Description: ax-ext with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010)

	Ref	Expression
Assertion	axextdist	|- ( ( -. A. z z = x /\ -. A. z z = y ) -> ( A. z ( z e. x <-> z e. y ) -> x = y ) )

Proof

Step	Hyp	Ref	Expression
1		nfnae	|- F/ z -. A. z z = x
2		nfnae	|- F/ z -. A. z z = y
3	1 2	nfan	|- F/ z ( -. A. z z = x /\ -. A. z z = y )
4		nfcvf	|- ( -. A. z z = x -> F/_ z x )
5	4	adantr	|- ( ( -. A. z z = x /\ -. A. z z = y ) -> F/_ z x )
6	5	nfcrd	|- ( ( -. A. z z = x /\ -. A. z z = y ) -> F/ z w e. x )
7		nfcvf	|- ( -. A. z z = y -> F/_ z y )
8	7	adantl	|- ( ( -. A. z z = x /\ -. A. z z = y ) -> F/_ z y )
9	8	nfcrd	|- ( ( -. A. z z = x /\ -. A. z z = y ) -> F/ z w e. y )
10	6 9	nfbid	|- ( ( -. A. z z = x /\ -. A. z z = y ) -> F/ z ( w e. x <-> w e. y ) )
11		elequ1	|- ( w = z -> ( w e. x <-> z e. x ) )
12		elequ1	|- ( w = z -> ( w e. y <-> z e. y ) )
13	11 12	bibi12d	|- ( w = z -> ( ( w e. x <-> w e. y ) <-> ( z e. x <-> z e. y ) ) )
14	13	a1i	|- ( ( -. A. z z = x /\ -. A. z z = y ) -> ( w = z -> ( ( w e. x <-> w e. y ) <-> ( z e. x <-> z e. y ) ) ) )
15	3 10 14	cbvald	|- ( ( -. A. z z = x /\ -. A. z z = y ) -> ( A. w ( w e. x <-> w e. y ) <-> A. z ( z e. x <-> z e. y ) ) )
16		axextg	|- ( A. w ( w e. x <-> w e. y ) -> x = y )
17	15 16	syl6bir	|- ( ( -. A. z z = x /\ -. A. z z = y ) -> ( A. z ( z e. x <-> z e. y ) -> x = y ) )