![]() |
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 2857 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶) | |
2 | 1 | neqned 2946 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∈ wcel 2106 ≠ wne 2939 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2723 df-clel 2809 df-ne 2940 |
This theorem is referenced by: elnelne1 3056 difsnb 4802 fofinf1o 9310 fin23lem24 10299 fin23lem31 10320 ttukeylem7 10492 npomex 10973 lbspss 20642 islbs3 20717 lbsextlem4 20723 obslbs 21218 hauspwpwf1 23420 ppiltx 26608 tglineneq 27760 lnopp2hpgb 27879 colopp 27885 ex-pss 29546 mxidlmaxv 32433 mxidlprm 32435 qsdrnglem2 32454 unelldsys 32985 cntnevol 33055 fin2solem 36276 lshpnelb 37657 osumcllem10N 38639 pexmidlem7N 38650 dochsnkrlem1 40143 ricdrng1 40904 rpnnen3lem 41539 lvecpsslmod 46834 |
Copyright terms: Public domain | W3C validator |