Theorem elqtop2

Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015)

	Ref	Expression
Hypothesis	qtoptop.1	|- X = U. J
Assertion	elqtop2	|- ( ( J e. V /\ F : X -onto-> Y ) -> ( A e. ( J qTop F ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )

Proof

Step	Hyp	Ref	Expression
1		qtoptop.1	|- X = U. J
2		ssid	|- X C_ X
3	1	elqtop	|- ( ( J e. V /\ F : X -onto-> Y /\ X C_ X ) -> ( A e. ( J qTop F ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )
4	2 3	mp3an3	|- ( ( J e. V /\ F : X -onto-> Y ) -> ( A e. ( J qTop F ) <-> ( A C_ Y /\ ( `' F " A ) e. J ) ) )