Theorem nelne2 3057

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-clel 2839  df-ne 2960

This theorem is referenced by:  nelelne  3058  elnelne2  3075  elneeldif  3920  elpwdifsn  4751  f1ounsn  7258  ac5num  9994  infpssrlem4  10265  fpwwe2lem12  10602  zgt1rpn0n1  13038  cats1un  14736  dprdfadd  20064  dprdcntz2  20082  lbsextlem4  21233  lindff1  21874  hauscmplem  23468  fileln0  23912  zcld  24876  dvcnvlem  26040  ppinprm  27218  chtnprm  27220  tglnpt4  28826  footexALT  28893  footexlem1  28894  footexlem2  28895  foot  28897  colperpexlem3  28907  mideulem2  28909  opphllem  28910  opphllem2  28923  lnopp2hpgb  28938  colhp  28945  lmieu  28959  trgcopy  28979  trgcopyeulem  28980  plngrotlem1  28996  plngrotlem2  28997  plngrot  28999  lnssplnglem  29000  cycpmco2lem1  33308  cycpmco2  33315  cyc3genpmlem  33333  unitnz  33421  fracfld  33497  linds2eq  33569  elrspunsn  33617  mxidlnzr  33657  lindsunlem  33923  fedgmul  33930  extdg1id  33965  2sqr3minply  34079  cos9thpiminplylem2  34082  ordtconnlem1  34223  esum2dlem  34391  subfacp1lem5  35539  mh-inf3f1  36906  heiborlem6  38320  llnle  40147  lplnle  40169  lhpexle1lem  40636  cdleme18b  40921  cdlemg46  41364  cdlemh  41446  ine1  42928  bcc0  44921  fnchoice  45614  climxrre  46329  stoweidlem43  46622  zneoALTV  48296  oppfrcllem  49753  oppfrcl2  49755  eloppf  49759