Theorem nelne1 3030

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-ne 2934

This theorem is referenced by:  elnelne1  3048  difsnb  4750  fofinf1o  9237  fin23lem24  10239  fin23lem31  10260  ttukeylem7  10432  npomex  10914  lbspss  21073  islbs3  21149  lbsextlem4  21155  obslbs  21724  hauspwpwf1  23966  ppiltx  27158  tglineneq  28730  lnopp2hpgb  28849  colopp  28855  ex-pss  30517  drngidlhash  33513  ssdifidlprm  33537  mxidlmaxv  33547  mxidlprm  33549  drnglidl1ne0  33554  drng0mxidl  33555  qsdrnglem2  33575  rsprprmprmidl  33601  1arithufdlem4  33626  ply1annnr  33867  irngnminplynz  33876  algextdeglem4  33884  unelldsys  34322  cntnevol  34392  fin2solem  37945  lshpnelb  39448  osumcllem10N  40429  pexmidlem7N  40440  dochsnkrlem1  41933  ricdrng1  42991  rpnnen3lem  43481  lvecpsslmod  48999