Theorem fvline2

Description: Alternate definition of a line. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	fvline2	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( A Line B ) = { x e. ( EE ` N ) | x Colinear <. A , B >. } )

Proof

Step	Hyp	Ref	Expression
1		fvline	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( A Line B ) = { x | x Colinear <. A , B >. } )
2		liness	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( A Line B ) C_ ( EE ` N ) )
3	1 2	eqsstrrd	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> { x | x Colinear <. A , B >. } C_ ( EE ` N ) )
4		dfss2	|- ( { x | x Colinear <. A , B >. } C_ ( EE ` N ) <-> ( { x | x Colinear <. A , B >. } i^i ( EE ` N ) ) = { x | x Colinear <. A , B >. } )
5	3 4	sylib	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( { x | x Colinear <. A , B >. } i^i ( EE ` N ) ) = { x | x Colinear <. A , B >. } )
6	1 5	eqtr4d	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( A Line B ) = ( { x | x Colinear <. A , B >. } i^i ( EE ` N ) ) )
7		dfrab2	|- { x e. ( EE ` N ) | x Colinear <. A , B >. } = ( { x | x Colinear <. A , B >. } i^i ( EE ` N ) )
8	6 7	eqtr4di	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( A Line B ) = { x e. ( EE ` N ) | x Colinear <. A , B >. } )