Theorem nelne1 3115

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∈ wcel 2114   ≠ wne 3018

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895  df-ne 3019

This theorem is referenced by:  elnelne1  3135  difsnb  4741  fofinf1o  8801  fin23lem24  9746  fin23lem31  9767  ttukeylem7  9939  npomex  10420  lbspss  19856  islbs3  19929  lbsextlem4  19935  obslbs  20876  hauspwpwf1  22597  ppiltx  25756  tglineneq  26432  lnopp2hpgb  26551  colopp  26557  ex-pss  28209  mxidlprm  30979  unelldsys  31419  cntnevol  31489  fin2solem  34880  lshpnelb  36122  osumcllem10N  37103  pexmidlem7N  37114  dochsnkrlem1  38607  rpnnen3lem  39635  lvecpsslmod  44569