Theorem nelne2 3030

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-ne 2933

This theorem is referenced by:  nelelne  3031  elnelne2  3048  elneeldif  3940  elpwdifsn  4765  f1ounsn  7264  ac5num  10048  infpssrlem4  10318  fpwwe2lem12  10654  zgt1rpn0n1  13048  cats1un  14737  dprdfadd  20001  dprdcntz2  20019  lbsextlem4  21120  lindff1  21778  hauscmplem  23342  fileln0  23786  zcld  24751  dvcnvlem  25930  ppinprm  27112  chtnprm  27114  footexALT  28643  footexlem1  28644  footexlem2  28645  foot  28647  colperpexlem3  28657  mideulem2  28659  opphllem  28660  opphllem2  28673  lnopp2hpgb  28688  colhp  28695  lmieu  28709  trgcopy  28729  trgcopyeulem  28730  cycpmco2lem1  33083  cycpmco2  33090  cyc3genpmlem  33108  unitnz  33180  fracfld  33248  linds2eq  33342  elrspunsn  33390  mxidlnzr  33428  lindsunlem  33610  fedgmul  33617  extdg1id  33653  2sqr3minply  33760  cos9thpiminplylem2  33763  ordtconnlem1  33901  esum2dlem  34069  subfacp1lem5  35152  heiborlem6  37786  llnle  39483  lplnle  39505  lhpexle1lem  39972  cdleme18b  40257  cdlemg46  40700  cdlemh  40782  ine1  42310  bcc0  44312  fnchoice  45001  climxrre  45727  stoweidlem43  46020  zneoALTV  47631  oppfrcllem  49023  oppfrcl2  49025