Theorem nelne2 3031

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-ne 2934

This theorem is referenced by:  nelelne  3032  elnelne2  3049  elneeldif  3917  elpwdifsn  4747  f1ounsn  7230  ac5num  9960  infpssrlem4  10230  fpwwe2lem12  10567  zgt1rpn0n1  12962  cats1un  14658  dprdfadd  19968  dprdcntz2  19986  lbsextlem4  21133  lindff1  21792  hauscmplem  23367  fileln0  23811  zcld  24775  dvcnvlem  25953  ppinprm  27135  chtnprm  27137  footexALT  28808  footexlem1  28809  footexlem2  28810  foot  28812  colperpexlem3  28822  mideulem2  28824  opphllem  28825  opphllem2  28838  lnopp2hpgb  28853  colhp  28860  lmieu  28874  trgcopy  28894  trgcopyeulem  28895  cycpmco2lem1  33226  cycpmco2  33233  cyc3genpmlem  33251  unitnz  33339  fracfld  33408  linds2eq  33480  elrspunsn  33528  mxidlnzr  33566  lindsunlem  33808  fedgmul  33815  extdg1id  33850  2sqr3minply  33964  cos9thpiminplylem2  33967  ordtconnlem1  34108  esum2dlem  34276  subfacp1lem5  35406  heiborlem6  38096  llnle  39923  lplnle  39945  lhpexle1lem  40412  cdleme18b  40697  cdlemg46  41140  cdlemh  41222  ine1  42713  bcc0  44725  fnchoice  45418  climxrre  46137  stoweidlem43  46430  zneoALTV  48058  oppfrcllem  49515  oppfrcl2  49517  eloppf  49521