Theorem nelne1 3040

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-ne 2943

This theorem is referenced by:  elnelne1  3058  difsnb  4736  fofinf1o  9024  fin23lem24  10009  fin23lem31  10030  ttukeylem7  10202  npomex  10683  lbspss  20259  islbs3  20332  lbsextlem4  20338  obslbs  20847  hauspwpwf1  23046  ppiltx  26231  tglineneq  26909  lnopp2hpgb  27028  colopp  27034  ex-pss  28693  mxidlprm  31542  unelldsys  32026  cntnevol  32096  fin2solem  35690  lshpnelb  36925  osumcllem10N  37906  pexmidlem7N  37917  dochsnkrlem1  39410  rpnnen3lem  40769  lvecpsslmod  45736