Theorem eltop2

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

	Ref	Expression
Assertion	eltop2	|- ( J e. Top -> ( A e. J <-> A. x e. A E. y e. J ( x e. y /\ y C_ A ) ) )

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		eltg2b	|- ( J e. Top -> ( A e. ( topGen ` J ) <-> A. x e. A E. y e. J ( x e. y /\ y C_ A ) ) )
4	2 3	bitr3d	|- ( J e. Top -> ( A e. J <-> A. x e. A E. y e. J ( x e. y /\ y C_ A ) ) )