Theorem nelne1 3029

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

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

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-ne 2933

This theorem is referenced by:  elnelne1  3047  difsnb  4782  fofinf1o  9342  fin23lem24  10334  fin23lem31  10355  ttukeylem7  10527  npomex  11008  lbspss  21038  islbs3  21114  lbsextlem4  21120  obslbs  21688  hauspwpwf1  23923  ppiltx  27137  tglineneq  28569  lnopp2hpgb  28688  colopp  28694  ex-pss  30355  drngidlhash  33395  ssdifidlprm  33419  mxidlmaxv  33429  mxidlprm  33431  drnglidl1ne0  33436  drng0mxidl  33437  qsdrnglem2  33457  rsprprmprmidl  33483  1arithufdlem4  33508  ply1annnr  33683  irngnminplynz  33692  algextdeglem4  33700  unelldsys  34135  cntnevol  34205  fin2solem  37576  lshpnelb  38948  osumcllem10N  39930  pexmidlem7N  39941  dochsnkrlem1  41434  ricdrng1  42498  rpnnen3lem  43002  lvecpsslmod  48431