Theorem atpointN

Description: The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ispoint.a	|- A = ( Atoms ` K )
2		ispoint.p	|- P = ( Points ` K )
3		eqid	|- { X } = { X }
4		sneq	|- ( x = X -> { x } = { X } )
5	4	rspceeqv	|- ( ( X e. A /\ { X } = { X } ) -> E. x e. A { X } = { x } )
6	3 5	mpan2	|- ( X e. A -> E. x e. A { X } = { x } )
7	6	adantl	|- ( ( K e. D /\ X e. A ) -> E. x e. A { X } = { x } )
8	1 2	ispointN	|- ( K e. D -> ( { X } e. P <-> E. x e. A { X } = { x } ) )
9	8	adantr	|- ( ( K e. D /\ X e. A ) -> ( { X } e. P <-> E. x e. A { X } = { x } ) )
10	7 9	mpbird	|- ( ( K e. D /\ X e. A ) -> { X } e. P )