Theorem nelne2 3095

Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)

Assertion

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

Proof of Theorem nelne2

Step	Hyp	Ref	Expression
1		eleq1 2893	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
2	1	biimpcd 241	. . 3 ⊢ (𝐴 ∈ 𝐶 → (𝐴 = 𝐵 → 𝐵 ∈ 𝐶))
3	2	necon3bd 3012	. 2 ⊢ (𝐴 ∈ 𝐶 → (¬ 𝐵 ∈ 𝐶 → 𝐴 ≠ 𝐵))
4	3	imp 397	1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386   = wceq 1658   ∈ wcel 2166   ≠ wne 2998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-cleq 2817  df-clel 2820  df-ne 2999

This theorem is referenced by:  nelelne  3096  elnelne2  3112  elpwdifsn  4538  ac5num  9171  infpssrlem4  9442  fpwwe2lem13  9778  zgt1rpn0n1  12154  cats1un  13810  dprdfadd  18772  dprdcntz2  18790  lbsextlem4  19521  lindff1  20525  hauscmplem  21579  fileln0  22023  zcld  22985  dvcnvlem  24137  ppinprm  25290  chtnprm  25292  footex  26029  foot  26030  colperpexlem3  26040  mideulem2  26042  opphllem  26043  opphllem2  26056  lnopp2hpgb  26071  colhp  26078  lmieu  26092  trgcopy  26112  trgcopyeulem  26113  ordtconnlem1  30514  esum2dlem  30698  subfacp1lem5  31711  heiborlem6  34156  llnle  35592  lplnle  35614  lhpexle1lem  36081  cdleme18b  36366  cdlemg46  36809  cdlemh  36891  bcc0  39378  fnchoice  40005  climxrre  40776  stoweidlem43  41053  zneoALTV  42409