Theorem nelne1 3047

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 2877	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → ¬ 𝐵 = 𝐶)
2	1	neqned 2958	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2111   ≠ wne 2951

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-clel 2830  df-ne 2952

This theorem is referenced by:  elnelne1  3065  difsnb  4696  fofinf1o  8832  fin23lem24  9782  fin23lem31  9803  ttukeylem7  9975  npomex  10456  lbspss  19922  islbs3  19995  lbsextlem4  20001  obslbs  20495  hauspwpwf1  22687  ppiltx  25861  tglineneq  26537  lnopp2hpgb  26656  colopp  26662  ex-pss  28312  mxidlprm  31161  unelldsys  31645  cntnevol  31715  fin2solem  35323  lshpnelb  36560  osumcllem10N  37541  pexmidlem7N  37552  dochsnkrlem1  39045  rpnnen3lem  40345  lvecpsslmod  45281