Theorem en3lplem1

Description: Lemma for en3lp . (Contributed by Alan Sare, 28-Oct-2011)

	Ref	Expression
Assertion	en3lplem1	|- ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = A -> ( x i^i { A , B , C } ) =/= (/) ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	|- ( ( A e. B /\ B e. C /\ C e. A ) -> C e. A )
2		eleq2	|- ( x = A -> ( C e. x <-> C e. A ) )
3	1 2	syl5ibrcom	|- ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = A -> C e. x ) )
4		tpid3g	|- ( C e. A -> C e. { A , B , C } )
5	4	3ad2ant3	|- ( ( A e. B /\ B e. C /\ C e. A ) -> C e. { A , B , C } )
6		inelcm	|- ( ( C e. x /\ C e. { A , B , C } ) -> ( x i^i { A , B , C } ) =/= (/) )
7	5 6	sylan2	|- ( ( C e. x /\ ( A e. B /\ B e. C /\ C e. A ) ) -> ( x i^i { A , B , C } ) =/= (/) )
8	7	expcom	|- ( ( A e. B /\ B e. C /\ C e. A ) -> ( C e. x -> ( x i^i { A , B , C } ) =/= (/) ) )
9	3 8	syld	|- ( ( A e. B /\ B e. C /\ C e. A ) -> ( x = A -> ( x i^i { A , B , C } ) =/= (/) ) )