Theorem nelne2 3031

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-clel 2811  df-ne 2935

This theorem is referenced by:  nelelne  3032  elnelne2  3049  elneeldif  3855  elpwdifsn  4674  ac5num  9529  infpssrlem4  9799  fpwwe2lem12  10135  zgt1rpn0n1  12506  cats1un  14165  dprdfadd  19254  dprdcntz2  19272  lbsextlem4  20045  lindff1  20629  hauscmplem  22150  fileln0  22594  zcld  23558  dvcnvlem  24720  ppinprm  25881  chtnprm  25883  footexALT  26656  footexlem1  26657  footexlem2  26658  foot  26660  colperpexlem3  26670  mideulem2  26672  opphllem  26673  opphllem2  26686  lnopp2hpgb  26701  colhp  26708  lmieu  26722  trgcopy  26742  trgcopyeulem  26743  cycpmco2lem1  30962  cycpmco2  30969  cyc3genpmlem  30987  linds2eq  31139  mxidlnzr  31203  lindsunlem  31269  fedgmul  31276  extdg1id  31302  ordtconnlem1  31438  esum2dlem  31622  subfacp1lem5  32709  heiborlem6  35586  llnle  37144  lplnle  37166  lhpexle1lem  37633  cdleme18b  37918  cdlemg46  38361  cdlemh  38443  bcc0  41480  fnchoice  42094  climxrre  42817  stoweidlem43  43110  zneoALTV  44639