Theorem nelne1 3083

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2111   ≠ wne 2987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ne 2988

This theorem is referenced by:  elnelne1  3101  difsnb  4699  fofinf1o  8783  fin23lem24  9733  fin23lem31  9754  ttukeylem7  9926  npomex  10407  lbspss  19847  islbs3  19920  lbsextlem4  19926  obslbs  20419  hauspwpwf1  22592  ppiltx  25762  tglineneq  26438  lnopp2hpgb  26557  colopp  26563  ex-pss  28213  mxidlprm  31048  unelldsys  31527  cntnevol  31597  fin2solem  35043  lshpnelb  36280  osumcllem10N  37261  pexmidlem7N  37272  dochsnkrlem1  38765  rpnnen3lem  39972  lvecpsslmod  44916