**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 | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ( 𝐶 ∩ 𝐵 ) = ∅ ) → ¬ 𝐴 ∈ 𝐶 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | inelcm | ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐶 ∩ 𝐵 ) ≠ ∅ ) | |

2 | 1 | expcom | ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝐶 → ( 𝐶 ∩ 𝐵 ) ≠ ∅ ) ) |

3 | 2 | necon2bd | ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐶 ∩ 𝐵 ) = ∅ → ¬ 𝐴 ∈ 𝐶 ) ) |

4 | 3 | imp | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ( 𝐶 ∩ 𝐵 ) = ∅ ) → ¬ 𝐴 ∈ 𝐶 ) |