Theorem nelne1 3038

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

Step	Hyp	Ref	Expression
1		nelneq2 2857	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶)
2	1	neqned 2946	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)

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