Theorem nelne1 3023

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-ne 2927

This theorem is referenced by:  elnelne1  3041  difsnb  4773  fofinf1o  9290  fin23lem24  10282  fin23lem31  10303  ttukeylem7  10475  npomex  10956  lbspss  20996  islbs3  21072  lbsextlem4  21078  obslbs  21646  hauspwpwf1  23881  ppiltx  27094  tglineneq  28578  lnopp2hpgb  28697  colopp  28703  ex-pss  30364  drngidlhash  33412  ssdifidlprm  33436  mxidlmaxv  33446  mxidlprm  33448  drnglidl1ne0  33453  drng0mxidl  33454  qsdrnglem2  33474  rsprprmprmidl  33500  1arithufdlem4  33525  ply1annnr  33700  irngnminplynz  33709  algextdeglem4  33717  unelldsys  34155  cntnevol  34225  fin2solem  37607  lshpnelb  38984  osumcllem10N  39966  pexmidlem7N  39977  dochsnkrlem1  41470  ricdrng1  42523  rpnnen3lem  43027  lvecpsslmod  48500