Theorem nelne2 3041

Description: Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.) (Proof shortened by Wolf Lammen, 14-May-2023.)

Assertion

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

Proof of Theorem nelne2

Step	Hyp	Ref	Expression
1		nelneq 2863	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵)
2	1	neqned 2949	1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-ne 2943

This theorem is referenced by:  nelelne  3042  elnelne2  3059  elneeldif  3897  elpwdifsn  4719  ac5num  9723  infpssrlem4  9993  fpwwe2lem12  10329  zgt1rpn0n1  12700  cats1un  14362  dprdfadd  19538  dprdcntz2  19556  lbsextlem4  20338  lindff1  20937  hauscmplem  22465  fileln0  22909  zcld  23882  dvcnvlem  25045  ppinprm  26206  chtnprm  26208  footexALT  26983  footexlem1  26984  footexlem2  26985  foot  26987  colperpexlem3  26997  mideulem2  26999  opphllem  27000  opphllem2  27013  lnopp2hpgb  27028  colhp  27035  lmieu  27049  trgcopy  27069  trgcopyeulem  27070  cycpmco2lem1  31295  cycpmco2  31302  cyc3genpmlem  31320  linds2eq  31477  mxidlnzr  31541  lindsunlem  31607  fedgmul  31614  extdg1id  31640  ordtconnlem1  31776  esum2dlem  31960  subfacp1lem5  33046  heiborlem6  35901  llnle  37459  lplnle  37481  lhpexle1lem  37948  cdleme18b  38233  cdlemg46  38676  cdlemh  38758  bcc0  41847  fnchoice  42461  climxrre  43181  stoweidlem43  43474  zneoALTV  45009