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  4764  fofinf1o  9246  fin23lem24  10246  fin23lem31  10267  ttukeylem7  10439  npomex  10921  lbspss  21051  islbs3  21127  lbsextlem4  21133  obslbs  21702  hauspwpwf1  23948  ppiltx  27160  tglineneq  28734  lnopp2hpgb  28853  colopp  28859  ex-pss  30521  drngidlhash  33533  ssdifidlprm  33557  mxidlmaxv  33567  mxidlprm  33569  drnglidl1ne0  33574  drng0mxidl  33575  qsdrnglem2  33595  rsprprmprmidl  33621  1arithufdlem4  33646  ply1annnr  33887  irngnminplynz  33896  algextdeglem4  33904  unelldsys  34342  cntnevol  34412  fin2solem  37886  lshpnelb  39389  osumcllem10N  40370  pexmidlem7N  40381  dochsnkrlem1  41874  ricdrng1  42927  rpnnen3lem  43417  lvecpsslmod  48896