Theorem nelne1 3025

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-ne 2929

This theorem is referenced by:  elnelne1  3043  difsnb  4755  fofinf1o  9216  fin23lem24  10213  fin23lem31  10234  ttukeylem7  10406  npomex  10887  lbspss  21016  islbs3  21092  lbsextlem4  21098  obslbs  21667  hauspwpwf1  23902  ppiltx  27114  tglineneq  28622  lnopp2hpgb  28741  colopp  28747  ex-pss  30408  drngidlhash  33399  ssdifidlprm  33423  mxidlmaxv  33433  mxidlprm  33435  drnglidl1ne0  33440  drng0mxidl  33441  qsdrnglem2  33461  rsprprmprmidl  33487  1arithufdlem4  33512  ply1annnr  33716  irngnminplynz  33725  algextdeglem4  33733  unelldsys  34171  cntnevol  34241  fin2solem  37645  lshpnelb  39082  osumcllem10N  40063  pexmidlem7N  40074  dochsnkrlem1  41567  ricdrng1  42620  rpnnen3lem  43123  lvecpsslmod  48607