Theorem nelne1 3040

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∈ wcel 2107   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-ne 2942

This theorem is referenced by:  elnelne1  3058  difsnb  4810  fofinf1o  9327  fin23lem24  10317  fin23lem31  10338  ttukeylem7  10510  npomex  10991  lbspss  20693  islbs3  20768  lbsextlem4  20774  obslbs  21285  hauspwpwf1  23491  ppiltx  26681  tglineneq  27895  lnopp2hpgb  28014  colopp  28020  ex-pss  29681  drngidlhash  32552  mxidlmaxv  32584  mxidlprm  32586  drnglidl1ne0  32591  drng0mxidl  32592  qsdrnglem2  32610  ply1annnr  32764  irngnminplynz  32771  algextdeglem1  32772  unelldsys  33156  cntnevol  33226  fin2solem  36474  lshpnelb  37854  osumcllem10N  38836  pexmidlem7N  38847  dochsnkrlem1  40340  ricdrng1  41102  rpnnen3lem  41770  lvecpsslmod  47188