Theorem nelne1 3039

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-ne 2941

This theorem is referenced by:  elnelne1  3057  difsnb  4806  fofinf1o  9372  fin23lem24  10362  fin23lem31  10383  ttukeylem7  10555  npomex  11036  lbspss  21081  islbs3  21157  lbsextlem4  21163  obslbs  21750  hauspwpwf1  23995  ppiltx  27220  tglineneq  28652  lnopp2hpgb  28771  colopp  28777  ex-pss  30447  drngidlhash  33462  ssdifidlprm  33486  mxidlmaxv  33496  mxidlprm  33498  drnglidl1ne0  33503  drng0mxidl  33504  qsdrnglem2  33524  rsprprmprmidl  33550  1arithufdlem4  33575  ply1annnr  33746  irngnminplynz  33755  algextdeglem4  33761  unelldsys  34159  cntnevol  34229  fin2solem  37613  lshpnelb  38985  osumcllem10N  39967  pexmidlem7N  39978  dochsnkrlem1  41471  ricdrng1  42538  rpnnen3lem  43043  lvecpsslmod  48424