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