Theorem nelne1 3041

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2106   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816  df-ne 2944

This theorem is referenced by:  elnelne1  3059  difsnb  4739  fofinf1o  9094  fin23lem24  10078  fin23lem31  10099  ttukeylem7  10271  npomex  10752  lbspss  20344  islbs3  20417  lbsextlem4  20423  obslbs  20937  hauspwpwf1  23138  ppiltx  26326  tglineneq  27005  lnopp2hpgb  27124  colopp  27130  ex-pss  28792  mxidlprm  31640  unelldsys  32126  cntnevol  32196  fin2solem  35763  lshpnelb  36998  osumcllem10N  37979  pexmidlem7N  37990  dochsnkrlem1  39483  rpnnen3lem  40853  lvecpsslmod  45848