Description: A minimum element of a class has no elements in common with the class. (Contributed by NM, 22-Jun-1994) (Proof shortened by JJ, 14-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | minel | |- ( ( A e. B /\ ( C i^i B ) = (/) ) -> -. A e. C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inelcm | |- ( ( A e. C /\ A e. B ) -> ( C i^i B ) =/= (/) ) |
|
| 2 | 1 | expcom | |- ( A e. B -> ( A e. C -> ( C i^i B ) =/= (/) ) ) |
| 3 | 2 | necon2bd | |- ( A e. B -> ( ( C i^i B ) = (/) -> -. A e. C ) ) |
| 4 | 3 | imp | |- ( ( A e. B /\ ( C i^i B ) = (/) ) -> -. A e. C ) |