Theorem nelne1 3037

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 2945	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∈ wcel 2104   ≠ wne 2938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808  df-ne 2939

This theorem is referenced by:  elnelne1  3055  difsnb  4808  fofinf1o  9329  fin23lem24  10319  fin23lem31  10340  ttukeylem7  10512  npomex  10993  lbspss  20837  islbs3  20913  lbsextlem4  20919  obslbs  21504  hauspwpwf1  23711  ppiltx  26917  tglineneq  28162  lnopp2hpgb  28281  colopp  28287  ex-pss  29948  drngidlhash  32826  mxidlmaxv  32858  mxidlprm  32860  drnglidl1ne0  32865  drng0mxidl  32866  qsdrnglem2  32884  ply1annnr  33053  irngnminplynz  33060  algextdeglem4  33065  unelldsys  33454  cntnevol  33524  fin2solem  36777  lshpnelb  38157  osumcllem10N  39139  pexmidlem7N  39150  dochsnkrlem1  40643  ricdrng1  41406  rpnnen3lem  42072  lvecpsslmod  47275