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  4770  fofinf1o  9283  fin23lem24  10275  fin23lem31  10296  ttukeylem7  10468  npomex  10949  lbspss  20989  islbs3  21065  lbsextlem4  21071  obslbs  21639  hauspwpwf1  23874  ppiltx  27087  tglineneq  28571  lnopp2hpgb  28690  colopp  28696  ex-pss  30357  drngidlhash  33405  ssdifidlprm  33429  mxidlmaxv  33439  mxidlprm  33441  drnglidl1ne0  33446  drng0mxidl  33447  qsdrnglem2  33467  rsprprmprmidl  33493  1arithufdlem4  33518  ply1annnr  33693  irngnminplynz  33702  algextdeglem4  33710  unelldsys  34148  cntnevol  34218  fin2solem  37600  lshpnelb  38977  osumcllem10N  39959  pexmidlem7N  39970  dochsnkrlem1  41463  ricdrng1  42516  rpnnen3lem  43020  lvecpsslmod  48496