Theorem nelne2 3084

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2111   ≠ wne 2987

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ne 2988

This theorem is referenced by:  nelelne  3085  elnelne2  3102  elneeldif  3895  elpwdifsn  4682  ac5num  9447  infpssrlem4  9717  fpwwe2lem13  10053  zgt1rpn0n1  12418  cats1un  14074  dprdfadd  19135  dprdcntz2  19153  lbsextlem4  19926  lindff1  20509  hauscmplem  22011  fileln0  22455  zcld  23418  dvcnvlem  24579  ppinprm  25737  chtnprm  25739  footexALT  26512  footexlem1  26513  footexlem2  26514  foot  26516  colperpexlem3  26526  mideulem2  26528  opphllem  26529  opphllem2  26542  lnopp2hpgb  26557  colhp  26564  lmieu  26578  trgcopy  26598  trgcopyeulem  26599  cycpmco2lem1  30818  cycpmco2  30825  cyc3genpmlem  30843  linds2eq  30995  mxidlnzr  31047  lindsunlem  31108  fedgmul  31115  extdg1id  31141  ordtconnlem1  31277  esum2dlem  31461  subfacp1lem5  32544  heiborlem6  35254  llnle  36814  lplnle  36836  lhpexle1lem  37303  cdleme18b  37588  cdlemg46  38031  cdlemh  38113  bcc0  41044  fnchoice  41658  climxrre  42392  stoweidlem43  42685  zneoALTV  44187