Theorem eltop

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

	Ref	Expression
Assertion	eltop	|- ( J e. Top -> ( A e. J <-> A C_ U. ( J i^i ~P 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		eltg	|- ( J e. Top -> ( A e. ( topGen ` J ) <-> A C_ U. ( J i^i ~P A ) ) )
4	2 3	bitr3d	|- ( J e. Top -> ( A e. J <-> A C_ U. ( J i^i ~P A ) ) )