Theorem nelne1 3028

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 2828	. . . 4 ⊢ (𝐵 = 𝐶 → (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶))
2	1	biimpcd 239	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐵 = 𝐶 → 𝐴 ∈ 𝐶))
3	2	necon3bd 2946	. 2 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ 𝐶 → 𝐵 ≠ 𝐶))
4	3	imp 444	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2139   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-clel 2756  df-ne 2933

This theorem is referenced by:  elnelne1  3045  difsnb  4482  fofinf1o  8406  fin23lem24  9336  fin23lem31  9357  ttukeylem7  9529  npomex  10010  lbspss  19284  islbs3  19357  lbsextlem4  19363  obslbs  20276  hauspwpwf1  21992  ppiltx  25102  tglineneq  25738  lnopp2hpgb  25854  colopp  25860  ex-pss  27596  unelldsys  30530  cntnevol  30600  fin2solem  33708  lshpnelb  34774  osumcllem10N  35754  pexmidlem7N  35765  dochsnkrlem1  37260  rpnnen3lem  38100  lvecpsslmod  42806