Theorem t0sep

Description: Any two topologically indistinguishable points in a T_0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypothesis	ist0.1	|- X = U. J
Assertion	t0sep	|- ( ( J e. Kol2 /\ ( A e. X /\ B e. X ) ) -> ( A. x e. J ( A e. x <-> B e. x ) -> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		ist0.1	|- X = U. J
2	1	ist0	|- ( J e. Kol2 <-> ( J e. Top /\ A. y e. X A. z e. X ( A. x e. J ( y e. x <-> z e. x ) -> y = z ) ) )
3	2	simprbi	|- ( J e. Kol2 -> A. y e. X A. z e. X ( A. x e. J ( y e. x <-> z e. x ) -> y = z ) )
4		eleq1	|- ( y = A -> ( y e. x <-> A e. x ) )
5	4	bibi1d	|- ( y = A -> ( ( y e. x <-> z e. x ) <-> ( A e. x <-> z e. x ) ) )
6	5	ralbidv	|- ( y = A -> ( A. x e. J ( y e. x <-> z e. x ) <-> A. x e. J ( A e. x <-> z e. x ) ) )
7		eqeq1	|- ( y = A -> ( y = z <-> A = z ) )
8	6 7	imbi12d	|- ( y = A -> ( ( A. x e. J ( y e. x <-> z e. x ) -> y = z ) <-> ( A. x e. J ( A e. x <-> z e. x ) -> A = z ) ) )
9		eleq1	|- ( z = B -> ( z e. x <-> B e. x ) )
10	9	bibi2d	|- ( z = B -> ( ( A e. x <-> z e. x ) <-> ( A e. x <-> B e. x ) ) )
11	10	ralbidv	|- ( z = B -> ( A. x e. J ( A e. x <-> z e. x ) <-> A. x e. J ( A e. x <-> B e. x ) ) )
12		eqeq2	|- ( z = B -> ( A = z <-> A = B ) )
13	11 12	imbi12d	|- ( z = B -> ( ( A. x e. J ( A e. x <-> z e. x ) -> A = z ) <-> ( A. x e. J ( A e. x <-> B e. x ) -> A = B ) ) )
14	8 13	rspc2va	|- ( ( ( A e. X /\ B e. X ) /\ A. y e. X A. z e. X ( A. x e. J ( y e. x <-> z e. x ) -> y = z ) ) -> ( A. x e. J ( A e. x <-> B e. x ) -> A = B ) )
15	14	ancoms	|- ( ( A. y e. X A. z e. X ( A. x e. J ( y e. x <-> z e. x ) -> y = z ) /\ ( A e. X /\ B e. X ) ) -> ( A. x e. J ( A e. x <-> B e. x ) -> A = B ) )
16	3 15	sylan	|- ( ( J e. Kol2 /\ ( A e. X /\ B e. X ) ) -> ( A. x e. J ( A e. x <-> B e. x ) -> A = B ) )