Theorem nelne2 3046

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-ne 2947

This theorem is referenced by:  nelelne  3047  elnelne2  3064  elneeldif  3990  elpwdifsn  4814  ac5num  10105  infpssrlem4  10375  fpwwe2lem12  10711  zgt1rpn0n1  13098  cats1un  14769  dprdfadd  20064  dprdcntz2  20082  lbsextlem4  21186  lindff1  21863  hauscmplem  23435  fileln0  23879  zcld  24854  dvcnvlem  26034  ppinprm  27213  chtnprm  27215  footexALT  28744  footexlem1  28745  footexlem2  28746  foot  28748  colperpexlem3  28758  mideulem2  28760  opphllem  28761  opphllem2  28774  lnopp2hpgb  28789  colhp  28796  lmieu  28810  trgcopy  28830  trgcopyeulem  28831  cycpmco2lem1  33119  cycpmco2  33126  cyc3genpmlem  33144  unitnz  33219  fracfld  33275  linds2eq  33374  elrspunsn  33422  mxidlnzr  33460  lindsunlem  33637  fedgmul  33644  extdg1id  33676  2sqr3minply  33738  ordtconnlem1  33870  esum2dlem  34056  subfacp1lem5  35152  heiborlem6  37776  llnle  39475  lplnle  39497  lhpexle1lem  39964  cdleme18b  40249  cdlemg46  40692  cdlemh  40774  ine1  42303  bcc0  44309  fnchoice  44929  climxrre  45671  stoweidlem43  45964  zneoALTV  47543