Theorem ispointN

Description: The predicate "is a point". (Contributed by NM, 2-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ispoint.a	|- A = ( Atoms ` K )
	ispoint.p	|- P = ( Points ` K )
Assertion	ispointN	|- ( K e. D -> ( X e. P <-> E. a e. A X = { a } ) )

Proof

Step	Hyp	Ref	Expression
1		ispoint.a	|- A = ( Atoms ` K )
2		ispoint.p	|- P = ( Points ` K )
3	1 2	pointsetN	|- ( K e. D -> P = { x | E. a e. A x = { a } } )
4	3	eleq2d	|- ( K e. D -> ( X e. P <-> X e. { x | E. a e. A x = { a } } ) )
5		vsnex	|- { a } e. _V
6		eleq1	|- ( X = { a } -> ( X e. _V <-> { a } e. _V ) )
7	5 6	mpbiri	|- ( X = { a } -> X e. _V )
8	7	rexlimivw	|- ( E. a e. A X = { a } -> X e. _V )
9		eqeq1	|- ( x = X -> ( x = { a } <-> X = { a } ) )
10	9	rexbidv	|- ( x = X -> ( E. a e. A x = { a } <-> E. a e. A X = { a } ) )
11	8 10	elab3	|- ( X e. { x | E. a e. A x = { a } } <-> E. a e. A X = { a } )
12	4 11	bitrdi	|- ( K e. D -> ( X e. P <-> E. a e. A X = { a } ) )