Theorem axext4dist 13867

Description: axext4 1869 with distinctors instead of distinct variable restrictions.

Assertion

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

Proof of Theorem axext4dist

Step	Hyp	Ref	Expression
1		ax-12 1310	. . . 4 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
2	1	imp 377	. . 3 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> A.z x = y))
3		hbnae 1507	. . . . 5 |- (-. A.z z = x -> A.z -. A.z z = x)
4		hbnae 1507	. . . . 5 |- (-. A.z z = y -> A.z -. A.z z = y)
5	3, 4	hban 1356	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> A.z(-. A.z z = x /\ -. A.z z = y))
6		elequ2 1497	. . . . 5 |- (x = y -> (z e. x <-> z e. y))
7	6	a1i 8	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> (z e. x <-> z e. y)))
8	5, 7	alimd 1343	. . 3 |- ((-. A.z z = x /\ -. A.z z = y) -> (A.z x = y -> A.z(z e. x <-> z e. y)))
9	2, 8	syld 30	. 2 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> A.z(z e. x <-> z e. y)))
10		axextdist 13866	. 2 |- ((-. A.z z = x /\ -. A.z z = y) -> (A.z(z e. x <-> z e. y) -> x = y))
11	9, 10	impbid 574	1 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y <-> A.z(z e. x <-> z e. y)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain