Theorem kqfeq

Description: Two points in the Kolmogorov quotient are equal iff the original points are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015)

	Ref	Expression
Hypothesis	kqval.2	|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion	kqfeq	|- ( ( J e. V /\ A e. X /\ B e. X ) -> ( ( F ` A ) = ( F ` B ) <-> A. y e. J ( A e. y <-> B e. y ) ) )

Proof

Step	Hyp	Ref	Expression
1		kqval.2	|- F = ( x e. X |-> { y e. J | x e. y } )
2	1	kqfval	|- ( ( J e. V /\ A e. X ) -> ( F ` A ) = { y e. J | A e. y } )
3	2	3adant3	|- ( ( J e. V /\ A e. X /\ B e. X ) -> ( F ` A ) = { y e. J | A e. y } )
4	1	kqfval	|- ( ( J e. V /\ B e. X ) -> ( F ` B ) = { y e. J | B e. y } )
5	4	3adant2	|- ( ( J e. V /\ A e. X /\ B e. X ) -> ( F ` B ) = { y e. J | B e. y } )
6	3 5	eqeq12d	|- ( ( J e. V /\ A e. X /\ B e. X ) -> ( ( F ` A ) = ( F ` B ) <-> { y e. J | A e. y } = { y e. J | B e. y } ) )
7		rabbi	|- ( A. y e. J ( A e. y <-> B e. y ) <-> { y e. J | A e. y } = { y e. J | B e. y } )
8	6 7	bitr4di	|- ( ( J e. V /\ A e. X /\ B e. X ) -> ( ( F ` A ) = ( F ` B ) <-> A. y e. J ( A e. y <-> B e. y ) ) )