Theorem nelne1 3029

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-ne 2933

This theorem is referenced by:  elnelne1  3047  difsnb  4751  fofinf1o  9242  fin23lem24  10244  fin23lem31  10265  ttukeylem7  10437  npomex  10919  lbspss  21077  islbs3  21153  lbsextlem4  21159  obslbs  21710  hauspwpwf1  23952  ppiltx  27140  tglineneq  28712  lnopp2hpgb  28831  colopp  28837  ex-pss  30498  drngidlhash  33494  ssdifidlprm  33518  mxidlmaxv  33528  mxidlprm  33530  drnglidl1ne0  33535  drng0mxidl  33536  qsdrnglem2  33556  rsprprmprmidl  33582  1arithufdlem4  33607  ply1annnr  33847  irngnminplynz  33856  algextdeglem4  33864  unelldsys  34302  cntnevol  34372  fin2solem  37927  lshpnelb  39430  osumcllem10N  40411  pexmidlem7N  40422  dochsnkrlem1  41915  ricdrng1  42973  rpnnen3lem  43459  lvecpsslmod  48983