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

Theorem nelne1 3113
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 2938 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → ¬ 𝐵 = 𝐶)
21neqned 3023 1 ((𝐴𝐵 ∧ ¬ 𝐴𝐶) → 𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wcel 2105  wne 3016
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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893  df-ne 3017
This theorem is referenced by:  elnelne1  3133  difsnb  4733  fofinf1o  8788  fin23lem24  9733  fin23lem31  9754  ttukeylem7  9926  npomex  10407  lbspss  19785  islbs3  19858  lbsextlem4  19864  obslbs  20804  hauspwpwf1  22525  ppiltx  25682  tglineneq  26358  lnopp2hpgb  26477  colopp  26483  ex-pss  28135  unelldsys  31317  cntnevol  31387  fin2solem  34760  lshpnelb  36002  osumcllem10N  36983  pexmidlem7N  36994  dochsnkrlem1  38487  rpnnen3lem  39508  lvecpsslmod  44460
  Copyright terms: Public domain W3C validator