Theorem eltop3

Description: Membership in a topology. (Contributed by NM, 19-Jul-2006)

	Ref	Expression
Assertion	eltop3	|- ( J e. Top -> ( A e. J <-> E. x ( x C_ J /\ A = U. x ) ) )

Proof

Step	Hyp	Ref	Expression
1		tgtop	|- ( J e. Top -> ( topGen ` J ) = J )
2	1	eleq2d	|- ( J e. Top -> ( A e. ( topGen ` J ) <-> A e. J ) )
3		eltg3	|- ( J e. Top -> ( A e. ( topGen ` J ) <-> E. x ( x C_ J /\ A = U. x ) ) )
4	2 3	bitr3d	|- ( J e. Top -> ( A e. J <-> E. x ( x C_ J /\ A = U. x ) ) )