Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nelne1 | Structured version Visualization version GIF version |
Description: Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.) |
Ref | Expression |
---|---|
nelne1 | ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nelneq2 2938 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶) | |
2 | 1 | neqned 3023 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∈ wcel 2105 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-clel 2893 df-ne 3017 |
This theorem is referenced by: elnelne1 3133 difsnb 4733 fofinf1o 8788 fin23lem24 9733 fin23lem31 9754 ttukeylem7 9926 npomex 10407 lbspss 19785 islbs3 19858 lbsextlem4 19864 obslbs 20804 hauspwpwf1 22525 ppiltx 25682 tglineneq 26358 lnopp2hpgb 26477 colopp 26483 ex-pss 28135 unelldsys 31317 cntnevol 31387 fin2solem 34760 lshpnelb 36002 osumcllem10N 36983 pexmidlem7N 36994 dochsnkrlem1 38487 rpnnen3lem 39508 lvecpsslmod 44460 |
Copyright terms: Public domain | W3C validator |