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  28667  footexlem1  28668  footexlem2  28669  foot  28671  colperpexlem3  28681  mideulem2  28683  opphllem  28684  opphllem2  28697  lnopp2hpgb  28712  colhp  28719  lmieu  28733  trgcopy  28753  trgcopyeulem  28754  cycpmco2lem1  33077  cycpmco2  33084  cyc3genpmlem  33102  unitnz  33188  fracfld  33256  linds2eq  33327  elrspunsn  33375  mxidlnzr  33413  lindsunlem  33607  fedgmul  33614  extdg1id  33649  2sqr3minply  33763  cos9thpiminplylem2  33766  ordtconnlem1  33907  esum2dlem  34075  subfacp1lem5  35177  heiborlem6  37816  llnle  39517  lplnle  39539  lhpexle1lem  40006  cdleme18b  40291  cdlemg46  40734  cdlemh  40816  ine1  42307  bcc0  44333  fnchoice  45027  climxrre  45751  stoweidlem43  46044  zneoALTV  47673  oppfrcllem  49132  oppfrcl2  49134  eloppf  49138