Theorem nelne1 2878

Description: Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)

Assertion

Ref	Expression
nelne1	⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)

Proof of Theorem nelne1

Step	Hyp	Ref	Expression
1		eleq2 2677	. . . 4 ⊢ (𝐵 = 𝐶 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
2	1	biimpcd 238	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐵 = 𝐶 → 𝐴 ∈ 𝐶))
3	2	necon3bd 2796	. 2 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ 𝐶 → 𝐵 ≠ 𝐶))
4	3	imp 444	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606  df-ne 2782

This theorem is referenced by:  elnelne1  2893  difsnb  4278  fofinf1o  8126  fin23lem24  9027  fin23lem31  9048  ttukeylem7  9220  npomex  9697  lbspss  18903  islbs3  18976  lbsextlem4  18982  obslbs  19893  hauspwpwf1  21601  ppiltx  24703  tglineneq  25339  lnopp2hpgb  25455  colopp  25461  ex-pss  26677  unelldsys  29548  cntnevol  29618  fin2solem  32565  lshpnelb  33289  osumcllem10N  34269  pexmidlem7N  34280  dochsnkrlem1  35776  rpnnen3lem  36616  lvecpsslmod  42090