Metamath Proof Explorer

Theorem linethrueu

Description: There is a unique line going through any two distinct points. Theorem 6.19 of Schwabhauser p. 46. (Contributed by Scott Fenton, 29-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion linethrueu 
|- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> E! x e. LinesEE ( P e. x /\ Q e. x ) )

Proof

Step Hyp Ref Expression
1 hilbert1.1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> E. x e. LinesEE ( P e. x /\ Q e. x ) )
2 simpr3 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> P =/= Q )
3 hilbert1.2 
 |-  ( P =/= Q -> E* x e. LinesEE ( P e. x /\ Q e. x ) )
4 2 3 syl 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> E* x e. LinesEE ( P e. x /\ Q e. x ) )
5 reu5 
 |-  ( E! x e. LinesEE ( P e. x /\ Q e. x ) <-> ( E. x e. LinesEE ( P e. x /\ Q e. x ) /\ E* x e. LinesEE ( P e. x /\ Q e. x ) ) )
6 1 4 5 sylanbrc 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> E! x e. LinesEE ( P e. x /\ Q e. x ) )