This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )