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  4763  fofinf1o  9236  fin23lem24  10236  fin23lem31  10257  ttukeylem7  10429  npomex  10911  lbspss  21038  islbs3  21114  lbsextlem4  21120  obslbs  21689  hauspwpwf1  23935  ppiltx  27147  tglineneq  28720  lnopp2hpgb  28839  colopp  28845  ex-pss  30507  drngidlhash  33517  ssdifidlprm  33541  mxidlmaxv  33551  mxidlprm  33553  drnglidl1ne0  33558  drng0mxidl  33559  qsdrnglem2  33579  rsprprmprmidl  33605  1arithufdlem4  33630  ply1annnr  33862  irngnminplynz  33871  algextdeglem4  33879  unelldsys  34317  cntnevol  34387  fin2solem  37809  lshpnelb  39312  osumcllem10N  40293  pexmidlem7N  40304  dochsnkrlem1  41797  ricdrng1  42850  rpnnen3lem  43340  lvecpsslmod  48820