MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nelne1 Structured version   Visualization version   GIF version

Theorem nelne1 3110
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.)
Assertion
Ref Expression
nelne1 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)

Proof of Theorem nelne1
StepHypRef Expression
1 nelneq2 2935 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → ¬ 𝐵 = 𝐶)
21neqned 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