Theorem nelne1 3045

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-ne 2947

This theorem is referenced by:  elnelne1  3063  difsnb  4831  fofinf1o  9400  fin23lem24  10391  fin23lem31  10412  ttukeylem7  10584  npomex  11065  lbspss  21104  islbs3  21180  lbsextlem4  21186  obslbs  21773  hauspwpwf1  24016  ppiltx  27238  tglineneq  28670  lnopp2hpgb  28789  colopp  28795  ex-pss  30460  drngidlhash  33427  ssdifidlprm  33451  mxidlmaxv  33461  mxidlprm  33463  drnglidl1ne0  33468  drng0mxidl  33469  qsdrnglem2  33489  rsprprmprmidl  33515  1arithufdlem4  33540  ply1annnr  33696  irngnminplynz  33705  algextdeglem4  33711  unelldsys  34122  cntnevol  34192  fin2solem  37566  lshpnelb  38940  osumcllem10N  39922  pexmidlem7N  39933  dochsnkrlem1  41426  ricdrng1  42483  rpnnen3lem  42988  lvecpsslmod  48236