Theorem nelne1 3022

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-ne 2926

This theorem is referenced by:  elnelne1  3040  difsnb  4766  fofinf1o  9259  fin23lem24  10251  fin23lem31  10272  ttukeylem7  10444  npomex  10925  lbspss  21021  islbs3  21097  lbsextlem4  21103  obslbs  21672  hauspwpwf1  23907  ppiltx  27120  tglineneq  28624  lnopp2hpgb  28743  colopp  28749  ex-pss  30407  drngidlhash  33398  ssdifidlprm  33422  mxidlmaxv  33432  mxidlprm  33434  drnglidl1ne0  33439  drng0mxidl  33440  qsdrnglem2  33460  rsprprmprmidl  33486  1arithufdlem4  33511  ply1annnr  33686  irngnminplynz  33695  algextdeglem4  33703  unelldsys  34141  cntnevol  34211  fin2solem  37593  lshpnelb  38970  osumcllem10N  39952  pexmidlem7N  39963  dochsnkrlem1  41456  ricdrng1  42509  rpnnen3lem  43013  lvecpsslmod  48489