Theorem nelne1 3022

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2109   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-ne 2926

This theorem is referenced by:  elnelne1  3040  difsnb  4757  fofinf1o  9222  fin23lem24  10216  fin23lem31  10237  ttukeylem7  10409  npomex  10890  lbspss  20986  islbs3  21062  lbsextlem4  21068  obslbs  21637  hauspwpwf1  23872  ppiltx  27085  tglineneq  28589  lnopp2hpgb  28708  colopp  28714  ex-pss  30372  drngidlhash  33372  ssdifidlprm  33396  mxidlmaxv  33406  mxidlprm  33408  drnglidl1ne0  33413  drng0mxidl  33414  qsdrnglem2  33434  rsprprmprmidl  33460  1arithufdlem4  33485  ply1annnr  33676  irngnminplynz  33685  algextdeglem4  33693  unelldsys  34131  cntnevol  34201  fin2solem  37596  lshpnelb  38973  osumcllem10N  39954  pexmidlem7N  39965  dochsnkrlem1  41458  ricdrng1  42511  rpnnen3lem  43014  lvecpsslmod  48502