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 2935 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶) | |
2 | 1 | neqned 3020 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∈ wcel 2105 ≠ wne 3013 |
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 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 df-ne 3014 |
This theorem is referenced by: elnelne1 3130 difsnb 4731 fofinf1o 8787 fin23lem24 9732 fin23lem31 9753 ttukeylem7 9925 npomex 10406 lbspss 19783 islbs3 19856 lbsextlem4 19862 obslbs 20802 hauspwpwf1 22523 ppiltx 25681 tglineneq 26357 lnopp2hpgb 26476 colopp 26482 ex-pss 28134 unelldsys 31316 cntnevol 31386 fin2solem 34759 lshpnelb 36000 osumcllem10N 36981 pexmidlem7N 36992 dochsnkrlem1 38485 rpnnen3lem 39506 lvecpsslmod 44490 |
Copyright terms: Public domain | W3C validator |