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  3904  elpwdifsn  4733  f1ounsn  7222  ac5num  9953  infpssrlem4  10223  fpwwe2lem12  10560  zgt1rpn0n1  12980  cats1un  14678  dprdfadd  19992  dprdcntz2  20010  lbsextlem4  21155  lindff1  21814  hauscmplem  23385  fileln0  23829  zcld  24793  dvcnvlem  25957  ppinprm  27133  chtnprm  27135  footexALT  28804  footexlem1  28805  footexlem2  28806  foot  28808  colperpexlem3  28818  mideulem2  28820  opphllem  28821  opphllem2  28834  lnopp2hpgb  28849  colhp  28856  lmieu  28870  trgcopy  28890  trgcopyeulem  28891  cycpmco2lem1  33206  cycpmco2  33213  cyc3genpmlem  33231  unitnz  33319  fracfld  33388  linds2eq  33460  elrspunsn  33508  mxidlnzr  33546  lindsunlem  33788  fedgmul  33795  extdg1id  33830  2sqr3minply  33944  cos9thpiminplylem2  33947  ordtconnlem1  34088  esum2dlem  34256  subfacp1lem5  35386  mh-inf3f1  36743  heiborlem6  38155  llnle  39982  lplnle  40004  lhpexle1lem  40471  cdleme18b  40756  cdlemg46  41199  cdlemh  41281  ine1  42764  bcc0  44789  fnchoice  45482  climxrre  46200  stoweidlem43  46493  zneoALTV  48161  oppfrcllem  49618  oppfrcl2  49620  eloppf  49624