| 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 2866 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶) | |
| 2 | 1 | neqned 2947 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∈ wcel 2108 ≠ wne 2940 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-clel 2816 df-ne 2941 |
| This theorem is referenced by: elnelne1 3057 difsnb 4806 fofinf1o 9372 fin23lem24 10362 fin23lem31 10383 ttukeylem7 10555 npomex 11036 lbspss 21081 islbs3 21157 lbsextlem4 21163 obslbs 21750 hauspwpwf1 23995 ppiltx 27220 tglineneq 28652 lnopp2hpgb 28771 colopp 28777 ex-pss 30447 drngidlhash 33462 ssdifidlprm 33486 mxidlmaxv 33496 mxidlprm 33498 drnglidl1ne0 33503 drng0mxidl 33504 qsdrnglem2 33524 rsprprmprmidl 33550 1arithufdlem4 33575 ply1annnr 33746 irngnminplynz 33755 algextdeglem4 33761 unelldsys 34159 cntnevol 34229 fin2solem 37613 lshpnelb 38985 osumcllem10N 39967 pexmidlem7N 39978 dochsnkrlem1 41471 ricdrng1 42538 rpnnen3lem 43043 lvecpsslmod 48424 |
| Copyright terms: Public domain | W3C validator |