Theorem nelne2 3023

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 2852	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → ¬ 𝐴 = 𝐵)
2	1	neqned 2932	1 ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-ne 2926

This theorem is referenced by:  nelelne  3024  elnelne2  3041  elneeldif  3917  elpwdifsn  4740  f1ounsn  7209  ac5num  9930  infpssrlem4  10200  fpwwe2lem12  10536  zgt1rpn0n1  12936  cats1un  14627  dprdfadd  19901  dprdcntz2  19919  lbsextlem4  21068  lindff1  21727  hauscmplem  23291  fileln0  23735  zcld  24700  dvcnvlem  25878  ppinprm  27060  chtnprm  27062  footexALT  28663  footexlem1  28664  footexlem2  28665  foot  28667  colperpexlem3  28677  mideulem2  28679  opphllem  28680  opphllem2  28693  lnopp2hpgb  28708  colhp  28715  lmieu  28729  trgcopy  28749  trgcopyeulem  28750  cycpmco2lem1  33069  cycpmco2  33076  cyc3genpmlem  33094  unitnz  33180  fracfld  33248  linds2eq  33319  elrspunsn  33367  mxidlnzr  33405  lindsunlem  33597  fedgmul  33604  extdg1id  33639  2sqr3minply  33753  cos9thpiminplylem2  33756  ordtconnlem1  33897  esum2dlem  34065  subfacp1lem5  35167  heiborlem6  37806  llnle  39507  lplnle  39529  lhpexle1lem  39996  cdleme18b  40281  cdlemg46  40724  cdlemh  40806  ine1  42297  bcc0  44323  fnchoice  45017  climxrre  45741  stoweidlem43  46034  zneoALTV  47663  oppfrcllem  49122  oppfrcl2  49124  eloppf  49128