Theorem nelne1 3033

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 2943	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∈ wcel 2121   ≠ wne 2936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816  df-ne 2937

This theorem is referenced by:  elnelne1  3051  difsnb  4742  fofinf1o  9236  fin23lem24  10239  fin23lem31  10260  ttukeylem7  10432  npomex  10914  lbspss  21076  islbs3  21152  lbsextlem4  21158  obslbs  21709  hauspwpwf1  23974  ppiltx  27162  tglineneq  28734  lnopp2hpgb  28853  colopp  28859  ex-pss  30520  drngidlhash  33521  ssdifidlprm  33545  mxidlmaxv  33555  mxidlprm  33557  drnglidl1ne0  33562  drng0mxidl  33563  qsdrnglem2  33583  dflringlem3  33591  dflring3  33592  dflring4  33593  rsprprmprmidl  33617  1arithufdlem4  33642  ply1annnr  33899  irngnminplynz  33908  algextdeglem4  33916  unelldsys  34354  cntnevol  34424  fin2solem  37988  lshpnelb  39491  osumcllem10N  40472  pexmidlem7N  40483  dochsnkrlem1  41976  ricdrng1  43029  rpnnen3lem  43491  lvecpsslmod  49012