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  3925  elpwdifsn  4749  f1ounsn  7229  ac5num  9965  infpssrlem4  10235  fpwwe2lem12  10571  zgt1rpn0n1  12970  cats1un  14662  dprdfadd  19936  dprdcntz2  19954  lbsextlem4  21103  lindff1  21762  hauscmplem  23326  fileln0  23770  zcld  24735  dvcnvlem  25913  ppinprm  27095  chtnprm  27097  footexALT  28698  footexlem1  28699  footexlem2  28700  foot  28702  colperpexlem3  28712  mideulem2  28714  opphllem  28715  opphllem2  28728  lnopp2hpgb  28743  colhp  28750  lmieu  28764  trgcopy  28784  trgcopyeulem  28785  cycpmco2lem1  33098  cycpmco2  33105  cyc3genpmlem  33123  unitnz  33206  fracfld  33274  linds2eq  33345  elrspunsn  33393  mxidlnzr  33431  lindsunlem  33613  fedgmul  33620  extdg1id  33654  2sqr3minply  33763  cos9thpiminplylem2  33766  ordtconnlem1  33907  esum2dlem  34075  subfacp1lem5  35164  heiborlem6  37803  llnle  39505  lplnle  39527  lhpexle1lem  39994  cdleme18b  40279  cdlemg46  40722  cdlemh  40804  ine1  42295  bcc0  44322  fnchoice  45016  climxrre  45741  stoweidlem43  46034  zneoALTV  47663  oppfrcllem  49109  oppfrcl2  49111  eloppf  49115