Theorem nelne1 3027

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809  df-ne 2931

This theorem is referenced by:  elnelne1  3045  difsnb  4760  fofinf1o  9230  fin23lem24  10230  fin23lem31  10251  ttukeylem7  10423  npomex  10905  lbspss  21032  islbs3  21108  lbsextlem4  21114  obslbs  21683  hauspwpwf1  23929  ppiltx  27141  tglineneq  28665  lnopp2hpgb  28784  colopp  28790  ex-pss  30452  drngidlhash  33464  ssdifidlprm  33488  mxidlmaxv  33498  mxidlprm  33500  drnglidl1ne0  33505  drng0mxidl  33506  qsdrnglem2  33526  rsprprmprmidl  33552  1arithufdlem4  33577  ply1annnr  33809  irngnminplynz  33818  algextdeglem4  33826  unelldsys  34264  cntnevol  34334  fin2solem  37746  lshpnelb  39183  osumcllem10N  40164  pexmidlem7N  40175  dochsnkrlem1  41668  ricdrng1  42725  rpnnen3lem  43215  lvecpsslmod  48695