Step |
Hyp |
Ref |
Expression |
1 |
|
disjif.1 |
|- F/_ x C |
2 |
|
disjif.2 |
|- ( x = Y -> B = C ) |
3 |
|
inelcm |
|- ( ( Z e. B /\ Z e. C ) -> ( B i^i C ) =/= (/) ) |
4 |
1 2
|
disji2f |
|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) /\ x =/= Y ) -> ( B i^i C ) = (/) ) |
5 |
4
|
3expia |
|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) ) -> ( x =/= Y -> ( B i^i C ) = (/) ) ) |
6 |
5
|
necon1d |
|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) ) -> ( ( B i^i C ) =/= (/) -> x = Y ) ) |
7 |
6
|
3impia |
|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) /\ ( B i^i C ) =/= (/) ) -> x = Y ) |
8 |
3 7
|
syl3an3 |
|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) /\ ( Z e. B /\ Z e. C ) ) -> x = Y ) |