Theorem nelne1 3056

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-clel 2839  df-ne 2960

This theorem is referenced by:  elnelne1  3074  difsnb  4768  fofinf1o  9277  fin23lem24  10281  fin23lem31  10302  ttukeylem7  10474  npomex  10956  lbspss  21151  islbs3  21227  lbsextlem4  21233  obslbs  21784  hauspwpwf1  24049  ppiltx  27243  tglineneq  28816  lnopp2hpgb  28938  colopp  28944  plngrotlem1  28996  plngrotlem2  28997  lnssplnglem  29000  ex-pss  30632  drngidlhash  33622  ssdifidlprm  33647  mxidlmaxv  33658  mxidlprm  33660  drnglidl1ne0  33665  drng0mxidl  33666  qsdrnglem2  33686  dflringlem3  33694  dflring3  33695  dflring4  33696  rsprprmprmidl  33720  1arithufdlem4  33745  ply1annnr  34002  irngnminplynz  34011  algextdeglem4  34019  unelldsys  34457  cntnevol  34527  fin2solem  38110  lshpnelb  39613  osumcllem10N  40594  pexmidlem7N  40605  dochsnkrlem1  42098  ricdrng1  43151  rpnnen3lem  43613  lvecpsslmod  49134