![]() |
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 2859 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶) | |
2 | 1 | neqned 2947 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 ∈ wcel 2107 ≠ wne 2940 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 df-clel 2811 df-ne 2941 |
This theorem is referenced by: elnelne1 3056 difsnb 4767 fofinf1o 9274 fin23lem24 10263 fin23lem31 10284 ttukeylem7 10456 npomex 10937 lbspss 20558 islbs3 20632 lbsextlem4 20638 obslbs 21152 hauspwpwf1 23354 ppiltx 26542 tglineneq 27628 lnopp2hpgb 27747 colopp 27753 ex-pss 29414 mxidlprm 32285 unelldsys 32814 cntnevol 32884 fin2solem 36110 lshpnelb 37492 osumcllem10N 38474 pexmidlem7N 38485 dochsnkrlem1 39978 ricdrng1 40762 rpnnen3lem 41398 lvecpsslmod 46674 |
Copyright terms: Public domain | W3C validator |