Theorem nelne1 3068

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 2868	. . . 4 ⊢ (𝐵 = 𝐶 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
2	1	biimpcd 241	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐵 = 𝐶 → 𝐴 ∈ 𝐶))
3	2	necon3bd 2986	. 2 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ 𝐶 → 𝐵 ≠ 𝐶))
4	3	imp 396	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 385   = wceq 1653   ∈ wcel 2157   ≠ wne 2972

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2778

This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2793  df-clel 2796  df-ne 2973

This theorem is referenced by:  elnelne1  3085  difsnb  4526  fofinf1o  8484  fin23lem24  9433  fin23lem31  9454  ttukeylem7  9626  npomex  10107  lbspss  19402  islbs3  19477  lbsextlem4  19483  obslbs  20398  hauspwpwf1  22118  ppiltx  25254  tglineneq  25894  lnopp2hpgb  26010  colopp  26016  ex-pss  27812  unelldsys  30736  cntnevol  30806  fin2solem  33883  lshpnelb  35004  osumcllem10N  35985  pexmidlem7N  35996  dochsnkrlem1  37489  rpnnen3lem  38378  lvecpsslmod  43090