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 } ) =/= (/) ) ) |